![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elrab | Unicode version |
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) |
Ref | Expression |
---|---|
elrab.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
elrab |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2319 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcv 2319 |
. 2
![]() ![]() ![]() ![]() | |
3 | nfv 1528 |
. 2
![]() ![]() ![]() ![]() | |
4 | elrab.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | elrabf 2891 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-rab 2464 df-v 2739 |
This theorem is referenced by: elrab3 2894 elrabd 2895 elrab2 2896 ralrab 2898 rexrab 2900 rabsnt 3667 unimax 3843 ssintub 3862 intminss 3869 exmidexmid 4195 exmidsssnc 4202 rabxfrd 4468 ordtri2or2exmidlem 4524 onsucelsucexmidlem1 4526 sefvex 5535 ssimaex 5576 acexmidlem2 5869 elpmg 6661 ssfilem 6872 diffitest 6884 inffiexmid 6903 supubti 6995 suplubti 6996 ctssexmid 7145 exmidonfinlem 7189 cc4f 7265 cc4n 7267 caucvgprlemladdfu 7673 caucvgprlemladdrl 7674 suplocexprlemmu 7714 suplocexprlemru 7715 suplocexprlemdisj 7716 suplocexprlemub 7719 nnindnn 7889 negf1o 8335 apsscn 8600 sup3exmid 8910 nnind 8931 peano2uz2 9356 peano5uzti 9357 dfuzi 9359 uzind 9360 uzind3 9362 eluz1 9528 uzind4 9584 supinfneg 9591 infsupneg 9592 eqreznegel 9610 elixx1 9893 elioo2 9917 elfz1 10009 expcl2lemap 10527 expclzaplem 10539 expclzap 10540 expap0i 10547 expge0 10551 expge1 10552 hashennnuni 10752 shftf 10832 reccn2ap 11314 dvdsdivcl 11848 divalgmod 11924 zsupcl 11940 infssuzex 11942 infssuzcldc 11944 bezoutlemsup 12002 dfgcd2 12007 uzwodc 12030 nnwosdc 12032 lcmcllem 12059 lcmledvds 12062 lcmgcdlem 12069 1nprm 12106 1idssfct 12107 isprm2 12109 phicl2 12206 hashdvds 12213 phisum 12232 odzval 12233 odzcllem 12234 odzdvds 12237 oddennn 12385 evenennn 12386 znnen 12391 ennnfonelemg 12396 ennnfonelemom 12401 ismhm 12785 issubm 12795 issubmd 12797 grplinv 12854 issubg 12964 isnsg 12993 issubrg 13280 istopon 13382 epttop 13461 iscld 13474 isnei 13515 neipsm 13525 iscn 13568 iscnp 13570 txdis1cn 13649 ishmeo 13675 ispsmet 13694 ismet 13715 isxmet 13716 elblps 13761 elbl 13762 xmetxpbl 13879 reopnap 13909 divcnap 13926 elcncf 13931 cdivcncfap 13958 cnopnap 13965 ellimc3apf 14000 limccoap 14018 dvlemap 14020 dvidlemap 14031 dvcnp2cntop 14034 dvaddxxbr 14036 dvmulxxbr 14037 dvcoapbr 14042 dvcjbr 14043 dvrecap 14048 dveflem 14058 lgsfle1 14281 lgsle1 14287 lgsdirprm 14306 lgsne0 14310 subctctexmid 14610 |
Copyright terms: Public domain | W3C validator |