![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfsbc1v | Structured version Visualization version Unicode 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 2603 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | nfsbc1 3298 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-sbc 3280 |
This theorem is referenced by: elrabsf 3318 cbvralcsf 3407 rabsnifsb 4053 euotd 4719 wfisg 5438 elfvmptrab1 5998 ralrnmpt 6059 oprabv 6371 elovmpt2rab 6547 elovmpt2rab1 6548 ovmpt3rabdm 6558 elovmpt3rab1 6559 tfindes 6721 findes 6755 dfopab2 6879 dfoprab3s 6880 mpt2xopoveq 6997 findcard2 7842 ac6sfi 7846 indexfi 7913 nn0ind-raph 11069 uzind4s 11253 fzrevral 11914 rabssnn0fi 12236 prmind2 14690 elmptrab 20897 isfildlem 20927 vtocl2d 28165 bnj919 29628 bnj1468 29707 bnj110 29719 bnj607 29777 bnj873 29785 bnj849 29786 bnj1388 29892 bnj1489 29915 setinds 30474 dfon2lem1 30479 tfisg 30507 frinsg 30533 indexa 32106 indexdom 32107 sdclem2 32117 sdclem1 32118 fdc1 32121 alrimii 32405 riotasv2s 32576 sbccomieg 35682 rexrabdioph 35683 rexfrabdioph 35684 aomclem6 35963 pm14.24 36828 gropd 39275 grstructd 39276 |
Copyright terms: Public domain | W3C validator |