![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elab2g | Structured version Visualization version GIF version |
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.) |
Ref | Expression |
---|---|
elab2g.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
elab2g.2 | ⊢ 𝐵 = {𝑥 ∣ 𝜑} |
Ref | Expression |
---|---|
elab2g | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elab2g.2 | . . 3 ⊢ 𝐵 = {𝑥 ∣ 𝜑} | |
2 | 1 | eleq2i 2821 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3665 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | bitrid 283 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 {cab 2705 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 |
This theorem is referenced by: elab2 3671 elab4g 3672 elrab 3682 eldif 3957 elin 3963 elun 4147 elpwg 4606 elsng 4643 elprg 4650 eluni 4911 elint 4955 elintg 4957 eliun 5000 eliin 5001 elopabw 5528 elxpi 5700 elrn2g 5893 eldmg 5901 dmopabelb 5919 elrnmpt 5958 elrnmpt1 5960 elimag 6067 elong 6377 elrnmpog 7556 elrnmpores 7559 eloprabi 8067 orderseqlem 8162 frrlem13 8303 tfrlem12 8409 elqsg 8786 fsetfocdm 8879 elixp2 8919 isacn 10067 isfin1a 10315 isfin2 10317 isfin4 10320 isfin7 10324 isfin3ds 10352 elwina 10709 elina 10710 iswun 10727 eltskg 10773 elgrug 10815 elnp 11010 elnpi 11011 iscat 17651 isps 18559 isdir 18589 ismgm 18600 elefmndbas2 18825 elsymgbas2 19326 mdetunilem9 22521 istopg 22796 isbasisg 22849 isptfin 23419 isufl 23816 isusp 24165 2sqlem9 27359 elno 27578 isuhgr 28872 isushgr 28873 isupgr 28896 isumgr 28907 isuspgr 28964 isusgr 28965 cplgruvtxb 29225 isconngr 29998 isconngr1 29999 isplig 30285 isgrpo 30306 elunop 31681 adjeu 31698 isarchi 32890 ispcmp 33458 eulerpartlemelr 33977 eulerpartlemgs2 34000 ballotlemfmpn 34114 isacycgr 34755 isacycgr1 34756 ismfs 35159 dfon2lem3 35381 elaltxp 35571 bj-ismoore 36584 heiborlem1 37284 heiborlem10 37293 isass 37319 isexid 37320 ismgmOLD 37323 elghomlem2OLD 37359 elcoeleqvrels 38067 eleldisjs 38200 gneispace2 43562 ismnu 43698 nzss 43754 elrnmptf 44554 issal 45702 ismea 45839 isome 45882 ismgmALT 47285 setrec1lem1 48118 |
Copyright terms: Public domain | W3C validator |