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 2825 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3572 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | syl5bb 286 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1542 ∈ wcel 2114 {cab 2717 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 |
This theorem is referenced by: elab2 3578 elab4g 3579 elrab 3589 eldif 3854 elin 3860 elun 4040 elpwg 4492 elsng 4531 elprg 4538 dfopif 4756 eluni 4800 elint 4843 elintg 4845 eliun 4886 eliin 4887 elopab 5383 elxpi 5548 elrn2g 5734 eldmg 5742 dmopabelb 5760 elrnmpt 5800 elrnmpt1 5802 elimag 5908 elong 6181 elrnmpog 7304 elrnmpores 7306 eloprabi 7789 tfrlem12 8057 elqsg 8382 fsetfocdm 8474 elixp2 8514 isacn 9547 isfin1a 9795 isfin2 9797 isfin4 9800 isfin7 9804 isfin3ds 9832 elwina 10189 elina 10190 iswun 10207 eltskg 10253 elgrug 10295 elnp 10490 elnpi 10491 iscat 17049 isps 17931 isdir 17961 ismgm 17972 elefmndbas2 18158 elsymgbas2 18622 mdetunilem9 21374 istopg 21649 isbasisg 21701 isptfin 22270 isufl 22667 isusp 23016 2sqlem9 26166 isuhgr 27008 isushgr 27009 isupgr 27032 isumgr 27043 isuspgr 27100 isusgr 27101 cplgruvtxb 27358 isconngr 28129 isconngr1 28130 isplig 28414 isgrpo 28435 elunop 29810 adjeu 29827 isarchi 31016 ispcmp 31382 eulerpartlemelr 31897 eulerpartlemgs2 31920 ballotlemfmpn 32034 isacycgr 32681 isacycgr1 32682 ismfs 33085 dfon2lem3 33338 orderseqlem 33417 frrlem13 33458 elno 33495 elaltxp 33923 bj-ismoore 34920 heiborlem1 35615 heiborlem10 35624 isass 35650 isexid 35651 ismgmOLD 35654 elghomlem2OLD 35690 elcoeleqvrels 36354 eleldisjs 36485 gneispace2 41311 ismnu 41444 nzss 41496 elrnmptf 42279 issal 43420 ismea 43554 isome 43597 ismgmALT 44981 setrec1lem1 45876 |
Copyright terms: Public domain | W3C validator |