![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsbc1v | Structured version Visualization version GIF version |
Description: Bound-variable hypothesis builder for class substitution. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Ref | Expression |
---|---|
nfsbc1v | ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2907 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | nfsbc1 3758 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1785 [wsbc 3739 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-sbc 3740 |
This theorem is referenced by: elrabsf 3787 cbvralcsf 3900 reusngf 4633 rexreusng 4640 reuprg0 4663 rmosn 4680 rabsnifsb 4683 euotd 5470 reuop 6245 frpoinsg 6297 wfisgOLD 6308 elfvmptrab1w 6974 elfvmptrab1 6975 ralrnmptw 7043 ralrnmpt 7045 oprabv 7416 elovmporab 7598 elovmporab1w 7599 elovmporab1 7600 ovmpt3rabdm 7611 elovmpt3rab1 7612 tfisg 7789 tfindes 7798 findes 7838 dfopab2 7983 dfoprab3s 7984 ralxpes 8067 ralxp3es 8070 frpoins3xpg 8071 frpoins3xp3g 8072 mpoxopoveq 8149 findcard2 9107 findcard2OLD 9227 ac6sfi 9230 indexfi 9303 frinsg 9686 nn0ind-raph 12602 uzind4s 12832 fzrevral 13525 rabssnn0fi 13890 prmind2 16560 elmptrab 23176 isfildlem 23206 2sqreulem4 26800 gropd 27929 grstructd 27930 rspc2daf 31344 opreu2reuALT 31352 bnj919 33319 bnj1468 33398 bnj110 33410 bnj607 33468 bnj873 33476 bnj849 33477 bnj1388 33585 bnj1489 33608 setinds 34293 dfon2lem1 34298 rdgssun 35839 indexa 36182 indexdom 36183 sdclem2 36191 sdclem1 36192 fdc1 36195 alrimii 36568 riotasv2s 37410 sbccomieg 41093 rexrabdioph 41094 rexfrabdioph 41095 aomclem6 41363 pm14.24 42693 or2expropbilem2 45238 or2expropbi 45239 ich2exprop 45634 ichnreuop 45635 ichreuopeq 45636 prproropreud 45672 reupr 45685 reuopreuprim 45689 |
Copyright terms: Public domain | W3C validator |