![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > elrab | GIF 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 2892 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ∈ wcel 2148 {crab 2459 |
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 2740 |
This theorem is referenced by: elrab3 2895 elrabd 2896 elrab2 2897 ralrab 2899 rexrab 2901 rabsnt 3668 unimax 3844 ssintub 3863 intminss 3870 exmidexmid 4197 exmidsssnc 4204 rabxfrd 4470 ordtri2or2exmidlem 4526 onsucelsucexmidlem1 4528 sefvex 5537 ssimaex 5578 acexmidlem2 5872 elpmg 6664 ssfilem 6875 diffitest 6887 inffiexmid 6906 supubti 6998 suplubti 6999 ctssexmid 7148 exmidonfinlem 7192 cc4f 7268 cc4n 7270 caucvgprlemladdfu 7676 caucvgprlemladdrl 7677 suplocexprlemmu 7717 suplocexprlemru 7718 suplocexprlemdisj 7719 suplocexprlemub 7722 nnindnn 7892 negf1o 8339 apsscn 8604 sup3exmid 8914 nnind 8935 peano2uz2 9360 peano5uzti 9361 dfuzi 9363 uzind 9364 uzind3 9366 eluz1 9532 uzind4 9588 supinfneg 9595 infsupneg 9596 eqreznegel 9614 elixx1 9897 elioo2 9921 elfz1 10013 expcl2lemap 10532 expclzaplem 10544 expclzap 10545 expap0i 10552 expge0 10556 expge1 10557 hashennnuni 10759 shftf 10839 reccn2ap 11321 dvdsdivcl 11856 divalgmod 11932 zsupcl 11948 infssuzex 11950 infssuzcldc 11952 bezoutlemsup 12010 dfgcd2 12015 uzwodc 12038 nnwosdc 12040 lcmcllem 12067 lcmledvds 12070 lcmgcdlem 12077 1nprm 12114 1idssfct 12115 isprm2 12117 phicl2 12214 hashdvds 12221 phisum 12240 odzval 12241 odzcllem 12242 odzdvds 12245 oddennn 12393 evenennn 12394 znnen 12399 ennnfonelemg 12404 ennnfonelemom 12409 ismhm 12853 issubm 12863 issubmd 12865 grplinv 12922 issubg 13033 isnsg 13062 issubrg 13342 istopon 13516 epttop 13593 iscld 13606 isnei 13647 neipsm 13657 iscn 13700 iscnp 13702 txdis1cn 13781 ishmeo 13807 ispsmet 13826 ismet 13847 isxmet 13848 elblps 13893 elbl 13894 xmetxpbl 14011 reopnap 14041 divcnap 14058 elcncf 14063 cdivcncfap 14090 cnopnap 14097 ellimc3apf 14132 limccoap 14150 dvlemap 14152 dvidlemap 14163 dvcnp2cntop 14166 dvaddxxbr 14168 dvmulxxbr 14169 dvcoapbr 14174 dvcjbr 14175 dvrecap 14180 dveflem 14190 lgsfle1 14413 lgsle1 14419 lgsdirprm 14438 lgsne0 14442 subctctexmid 14753 |
Copyright terms: Public domain | W3C validator |