Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > csbief | Structured version Visualization version Unicode version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 26-Nov-2005.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
csbief.1 | |
csbief.2 | |
csbief.3 |
Ref | Expression |
---|---|
csbief |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbief.1 | . 2 | |
2 | csbief.2 | . . . 4 | |
3 | 2 | a1i 11 | . . 3 |
4 | csbief.3 | . . 3 | |
5 | 3, 4 | csbiegf 3557 | . 2 |
6 | 1, 5 | ax-mp 5 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 wnfc 2751 cvv 3200 csb 3533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-sbc 3436 df-csb 3534 |
This theorem is referenced by: csbie 3559 csbun 4009 csbin 4010 csbif 4138 csbopab 5008 csbopabgALT 5009 csbima12 5483 csbiota 5881 csbriota 6623 csbov123 6687 pcmpt 15596 mpfrcl 19518 iundisj2 23317 iundisj2f 29403 iundisj2fi 29556 csbdif 33171 sbccom2f 33931 csbcog 37941 csbingOLD 39054 csbafv12g 41217 csbaovg 41260 |
Copyright terms: Public domain | W3C validator |