![]() |
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 2891 | 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 2739 |
This theorem is referenced by: elrab3 2894 elrabd 2895 elrab2 2896 ralrab 2898 rexrab 2900 rabsnt 3666 unimax 3841 ssintub 3860 intminss 3867 exmidexmid 4193 exmidsssnc 4200 rabxfrd 4466 ordtri2or2exmidlem 4522 onsucelsucexmidlem1 4524 sefvex 5532 ssimaex 5573 acexmidlem2 5866 elpmg 6658 ssfilem 6869 diffitest 6881 inffiexmid 6900 supubti 6992 suplubti 6993 ctssexmid 7142 exmidonfinlem 7186 cc4f 7259 cc4n 7261 caucvgprlemladdfu 7667 caucvgprlemladdrl 7668 suplocexprlemmu 7708 suplocexprlemru 7709 suplocexprlemdisj 7710 suplocexprlemub 7713 nnindnn 7883 negf1o 8329 apsscn 8594 sup3exmid 8903 nnind 8924 peano2uz2 9349 peano5uzti 9350 dfuzi 9352 uzind 9353 uzind3 9355 eluz1 9521 uzind4 9577 supinfneg 9584 infsupneg 9585 eqreznegel 9603 elixx1 9884 elioo2 9908 elfz1 10000 expcl2lemap 10518 expclzaplem 10530 expclzap 10531 expap0i 10538 expge0 10542 expge1 10543 hashennnuni 10743 shftf 10823 reccn2ap 11305 dvdsdivcl 11839 divalgmod 11915 zsupcl 11931 infssuzex 11933 infssuzcldc 11935 bezoutlemsup 11993 dfgcd2 11998 uzwodc 12021 nnwosdc 12023 lcmcllem 12050 lcmledvds 12053 lcmgcdlem 12060 1nprm 12097 1idssfct 12098 isprm2 12100 phicl2 12197 hashdvds 12204 phisum 12223 odzval 12224 odzcllem 12225 odzdvds 12228 oddennn 12376 evenennn 12377 znnen 12382 ennnfonelemg 12387 ennnfonelemom 12392 ismhm 12743 issubm 12753 issubmd 12755 grplinv 12812 istopon 13178 epttop 13257 iscld 13270 isnei 13311 neipsm 13321 iscn 13364 iscnp 13366 txdis1cn 13445 ishmeo 13471 ispsmet 13490 ismet 13511 isxmet 13512 elblps 13557 elbl 13558 xmetxpbl 13675 reopnap 13705 divcnap 13722 elcncf 13727 cdivcncfap 13754 cnopnap 13761 ellimc3apf 13796 limccoap 13814 dvlemap 13816 dvidlemap 13827 dvcnp2cntop 13830 dvaddxxbr 13832 dvmulxxbr 13833 dvcoapbr 13838 dvcjbr 13839 dvrecap 13844 dveflem 13854 lgsfle1 14077 lgsle1 14083 lgsdirprm 14102 lgsne0 14106 subctctexmid 14406 |
Copyright terms: Public domain | W3C validator |