![]() |
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 2851 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3556 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | syl5bb 275 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ∈ wcel 2107 {cab 2763 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 |
This theorem is referenced by: elab2 3562 elab4g 3563 elrab 3572 eldif 3802 elun 3976 elin 4019 elsng 4412 elprg 4419 eluni 4674 elintg 4718 eliun 4757 eliin 4758 elopab 5220 elrn2g 5558 eldmg 5564 elrnmpt 5618 elrnmpt1 5620 elimag 5724 elong 5984 elrnmpt2g 7049 elrnmpt2res 7051 eloprabi 7512 tfrlem12 7768 elqsg 8081 elixp2 8198 isacn 9200 isfin1a 9449 isfin2 9451 isfin4 9454 isfin7 9458 isfin3ds 9486 elwina 9843 elina 9844 iswun 9861 eltskg 9907 elgrug 9949 elnp 10144 elnpi 10145 iscat 16718 isps 17588 isdir 17618 ismgm 17629 elsymgbas2 18184 mdetunilem9 20831 istopg 21107 isbasisg 21159 isptfin 21728 isufl 22125 isusp 22473 2sqlem9 25604 isuhgr 26408 isushgr 26409 isupgr 26432 isumgr 26443 isuspgr 26501 isusgr 26502 cplgruvtxb 26761 isconngr 27592 isconngr1 27593 isfrgr 27666 isplig 27903 isgrpo 27924 elunop 29303 adjeu 29320 isarchi 30298 ispcmp 30522 eulerpartlemelr 31017 eulerpartlemgs2 31040 ballotlemfmpn 31155 ismfs 32045 dfon2lem3 32278 orderseqlem 32341 elno 32388 elaltxp 32671 bj-ismoore 33632 heiborlem1 34234 heiborlem10 34243 isass 34269 isexid 34270 ismgmOLD 34273 elghomlem2OLD 34309 gneispace2 39386 nzss 39472 elrnmptf 40290 issal 41458 isome 41635 ismgmALT 42874 setrec1lem1 43539 |
Copyright terms: Public domain | W3C validator |