| 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 2833 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
| 3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 4 | 3 | elabg 3676 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
| 5 | 2, 4 | bitrid 283 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 {cab 2714 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: elab2 3682 elab4g 3683 elrab 3692 eldif 3961 elin 3967 elun 4153 elpwg 4603 elsng 4640 elprg 4648 eluni 4910 elint 4952 elintg 4954 eliun 4995 eliin 4996 elopabw 5531 elxpi 5707 elrn2g 5901 eldmg 5909 dmopabelb 5927 elrnmpt 5969 elrnmpt1 5971 elimag 6082 elong 6392 elrnmpog 7568 elrnmpores 7571 eloprabi 8088 orderseqlem 8182 frrlem13 8323 tfrlem12 8429 elqsg 8808 fsetfocdm 8901 elixp2 8941 isacn 10084 isfin1a 10332 isfin2 10334 isfin4 10337 isfin7 10341 isfin3ds 10369 elwina 10726 elina 10727 iswun 10744 eltskg 10790 elgrug 10832 elnp 11027 elnpi 11028 iscat 17715 isps 18613 isdir 18643 ismgm 18654 elefmndbas2 18887 elsymgbas2 19390 mdetunilem9 22626 istopg 22901 isbasisg 22954 isptfin 23524 isufl 23921 isusp 24270 2sqlem9 27471 elno 27690 elnoOLD 27691 elzs12 28421 isuhgr 29077 isushgr 29078 isupgr 29101 isumgr 29112 isuspgr 29169 isusgr 29170 cplgruvtxb 29430 isconngr 30208 isconngr1 30209 isplig 30495 isgrpo 30516 elunop 31891 adjeu 31908 isarchi 33189 ispcmp 33856 eulerpartlemelr 34359 eulerpartlemgs2 34382 ballotlemfmpn 34497 isacycgr 35150 isacycgr1 35151 ismfs 35554 dfon2lem3 35786 elaltxp 35976 bj-ismoore 37106 heiborlem1 37818 heiborlem10 37827 isass 37853 isexid 37854 ismgmOLD 37857 elghomlem2OLD 37893 elcoeleqvrels 38596 eleldisjs 38729 gneispace2 44145 ismnu 44280 nzss 44336 elrnmptf 45186 issal 46329 ismea 46466 isome 46509 ismgmALT 48139 setrec1lem1 49206 |
| Copyright terms: Public domain | W3C validator |