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 2904 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3665 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | syl5bb 285 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1533 ∈ wcel 2110 {cab 2799 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 |
This theorem is referenced by: elab2 3669 elab4g 3670 elrab 3679 eldif 3945 elun 4124 elin 4168 elpwg 4544 elsng 4574 elprg 4581 eluni 4834 elintg 4876 eliun 4915 eliin 4916 elopab 5406 elrn2g 5755 eldmg 5761 dmopabelb 5779 elrnmpt 5822 elrnmpt1 5824 elimag 5927 elong 6193 elrnmpog 7280 elrnmpores 7282 eloprabi 7755 tfrlem12 8019 elqsg 8342 elixp2 8459 isacn 9464 isfin1a 9708 isfin2 9710 isfin4 9713 isfin7 9717 isfin3ds 9745 elwina 10102 elina 10103 iswun 10120 eltskg 10166 elgrug 10208 elnp 10403 elnpi 10404 iscat 16937 isps 17806 isdir 17836 ismgm 17847 elefmndbas2 18033 elsymgbas2 18495 mdetunilem9 21223 istopg 21497 isbasisg 21549 isptfin 22118 isufl 22515 isusp 22864 2sqlem9 25997 isuhgr 26839 isushgr 26840 isupgr 26863 isumgr 26874 isuspgr 26931 isusgr 26932 cplgruvtxb 27189 isconngr 27962 isconngr1 27963 isplig 28247 isgrpo 28268 elunop 29643 adjeu 29660 isarchi 30806 ispcmp 31116 eulerpartlemelr 31610 eulerpartlemgs2 31633 ballotlemfmpn 31747 isacycgr 32387 isacycgr1 32388 ismfs 32791 dfon2lem3 33025 orderseqlem 33089 frrlem13 33130 elno 33148 elaltxp 33431 bj-ismoore 34391 heiborlem1 35083 heiborlem10 35092 isass 35118 isexid 35119 ismgmOLD 35122 elghomlem2OLD 35158 elcoeleqvrels 35824 eleldisjs 35955 gneispace2 40475 ismnu 40590 nzss 40642 elrnmptf 41434 issal 42593 ismea 42727 isome 42770 ismgmALT 44124 setrec1lem1 44784 |
Copyright terms: Public domain | W3C validator |