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 2974 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | 1 | nfsbc1 3788 | 1 ⊢ Ⅎ𝑥[𝐴 / 𝑥]𝜑 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1775 [wsbc 3769 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-sbc 3770 |
This theorem is referenced by: elrabsf 3813 cbvralcsf 3922 vtocl2dOLD 3928 reusngf 4604 rexreusng 4609 reuprg0 4630 rmosn 4647 rabsnifsb 4650 euotd 5394 reuop 6137 wfisg 6176 elfvmptrab1w 6786 elfvmptrab1 6787 ralrnmptw 6852 ralrnmpt 6854 oprabv 7203 elovmporab 7380 elovmporab1w 7381 elovmporab1 7382 ovmpt3rabdm 7393 elovmpt3rab1 7394 tfindes 7566 findes 7601 dfopab2 7739 dfoprab3s 7740 mpoxopoveq 7874 findcard2 8746 ac6sfi 8750 indexfi 8820 nn0ind-raph 12070 uzind4s 12296 fzrevral 12980 rabssnn0fi 13342 prmind2 16017 elmptrab 22363 isfildlem 22393 2sqreulem4 25957 gropd 26743 grstructd 26744 rspc2daf 30158 opreu2reuALT 30167 bnj919 31937 bnj1468 32017 bnj110 32029 bnj607 32087 bnj873 32095 bnj849 32096 bnj1388 32202 bnj1489 32225 setinds 32920 dfon2lem1 32925 tfisg 32952 frpoinsg 32978 frinsg 32984 rdgssun 34541 indexa 34889 indexdom 34890 sdclem2 34898 sdclem1 34899 fdc1 34902 alrimii 35278 riotasv2s 35974 sbccomieg 39268 rexrabdioph 39269 rexfrabdioph 39270 aomclem6 39537 pm14.24 40641 or2expropbilem2 43145 or2expropbi 43146 ich2exprop 43510 ichnreuop 43511 ichreuopeq 43512 prproropreud 43548 reupr 43561 reuopreuprim 43565 |
Copyright terms: Public domain | W3C validator |