![]() |
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 2841 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3500 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | syl5bb 272 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1630 ∈ wcel 2144 {cab 2756 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1633 df-ex 1852 df-nf 1857 df-sb 2049 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-v 3351 |
This theorem is referenced by: elab2 3503 elab4g 3504 eldif 3731 elun 3902 elin 3945 elsng 4328 elprg 4334 eluni 4575 elintg 4617 eliun 4656 eliin 4657 elopab 5116 elrn2g 5451 eldmg 5457 elrnmpt 5510 elrnmpt1 5512 elimag 5611 elong 5874 elrnmpt2g 6918 elrnmpt2res 6920 eloprabi 7381 tfrlem12 7637 elqsg 7949 elixp2 8065 isacn 9066 isfin1a 9315 isfin2 9317 isfin4 9320 isfin7 9324 isfin3ds 9352 elwina 9709 elina 9710 iswun 9727 eltskg 9773 elgrug 9815 elnp 10010 elnpi 10011 iscat 16539 isps 17409 isdir 17439 ismgm 17450 elsymgbas2 18007 mdetunilem9 20643 istopg 20919 isbasisg 20971 isptfin 21539 isufl 21936 isusp 22284 2sqlem9 25372 isuhgr 26175 isushgr 26176 isupgr 26199 isumgr 26210 isuspgr 26268 isusgr 26269 cplgruvtxb 26542 isconngr 27366 isconngr1 27367 isfrgr 27437 isplig 27664 isgrpo 27685 elunop 29065 adjeu 29082 isarchi 30070 ispcmp 30258 eulerpartlemelr 30753 eulerpartlemgs2 30776 ballotlemfmpn 30890 ismfs 31778 dfon2lem3 32020 orderseqlem 32083 elno 32130 elaltxp 32413 bj-ismoore 33384 heiborlem1 33935 heiborlem10 33944 isass 33970 isexid 33971 ismgmOLD 33974 elghomlem2OLD 34010 gneispace2 38949 nzss 39035 elrnmptf 39881 issal 41045 isome 41222 ismgmALT 42377 setrec1lem1 42952 |
Copyright terms: Public domain | W3C validator |