![]() |
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 2282 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2282 | . 2 ⊢ Ⅎ𝑥𝐵 | |
3 | nfv 1509 | . 2 ⊢ Ⅎ𝑥𝜓 | |
4 | elrab.1 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 1, 2, 3, 4 | elrabf 2842 | 1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1332 ∈ wcel 1481 {crab 2421 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-nfc 2271 df-rab 2426 df-v 2691 |
This theorem is referenced by: elrab3 2845 elrabd 2846 elrab2 2847 ralrab 2849 rexrab 2851 rabsnt 3606 unimax 3778 ssintub 3797 intminss 3804 exmidexmid 4128 exmidsssnc 4134 rabxfrd 4398 ordtri2or2exmidlem 4449 onsucelsucexmidlem1 4451 sefvex 5450 ssimaex 5490 acexmidlem2 5779 elpmg 6566 ssfilem 6777 diffitest 6789 inffiexmid 6808 supubti 6894 suplubti 6895 ctssexmid 7032 exmidonfinlem 7066 cc4f 7101 cc4n 7103 caucvgprlemladdfu 7509 caucvgprlemladdrl 7510 suplocexprlemmu 7550 suplocexprlemru 7551 suplocexprlemdisj 7552 suplocexprlemub 7555 nnindnn 7725 negf1o 8168 apsscn 8433 sup3exmid 8739 nnind 8760 peano2uz2 9182 peano5uzti 9183 dfuzi 9185 uzind 9186 uzind3 9188 eluz1 9354 uzind4 9410 supinfneg 9417 infsupneg 9418 eqreznegel 9433 elixx1 9710 elioo2 9734 elfz1 9826 expcl2lemap 10336 expclzaplem 10348 expclzap 10349 expap0i 10356 expge0 10360 expge1 10361 hashennnuni 10557 shftf 10634 reccn2ap 11114 dvdsdivcl 11584 divalgmod 11660 zsupcl 11676 infssuzex 11678 infssuzcldc 11680 bezoutlemsup 11733 dfgcd2 11738 lcmcllem 11784 lcmledvds 11787 lcmgcdlem 11794 1nprm 11831 1idssfct 11832 isprm2 11834 phicl2 11926 hashdvds 11933 oddennn 11941 evenennn 11942 znnen 11947 ennnfonelemg 11952 ennnfonelemom 11957 istopon 12219 epttop 12298 iscld 12311 isnei 12352 neipsm 12362 iscn 12405 iscnp 12407 txdis1cn 12486 ishmeo 12512 ispsmet 12531 ismet 12552 isxmet 12553 elblps 12598 elbl 12599 xmetxpbl 12716 reopnap 12746 divcnap 12763 elcncf 12768 cdivcncfap 12795 cnopnap 12802 ellimc3apf 12837 limccoap 12855 dvlemap 12857 dvidlemap 12868 dvcnp2cntop 12871 dvaddxxbr 12873 dvmulxxbr 12874 dvcoapbr 12879 dvcjbr 12880 dvrecap 12885 dveflem 12895 subctctexmid 13369 |
Copyright terms: Public domain | W3C validator |