![]() |
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 2881 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3614 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | syl5bb 286 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 = wceq 1538 ∈ wcel 2111 {cab 2776 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 |
This theorem is referenced by: elab2 3618 elab4g 3619 elrab 3628 eliun 4885 eliin 4886 elopab 5379 elrn2g 5725 eldmg 5731 dmopabelb 5749 elrnmpt 5792 elrnmpt1 5794 elimag 5900 elrnmpog 7265 elrnmpores 7267 eloprabi 7743 tfrlem12 8008 elqsg 8331 elixp2 8448 isacn 9455 isfin1a 9703 isfin4 9708 isfin7 9712 isfin3ds 9740 elwina 10097 elina 10098 eltskg 10161 elgrug 10203 elnp 10398 iscat 16935 isps 17804 isdir 17834 ismgm 17845 elefmndbas2 18031 elsymgbas2 18493 mdetunilem9 21225 istopg 21500 isbasisg 21552 isptfin 22121 isufl 22518 isusp 22867 2sqlem9 26011 isuhgr 26853 isushgr 26854 isupgr 26877 isumgr 26888 isuspgr 26945 isusgr 26946 cplgruvtxb 27203 isconngr 27974 isconngr1 27975 isplig 28259 isgrpo 28280 elunop 29655 adjeu 29672 isarchi 30861 ispcmp 31210 eulerpartlemelr 31725 eulerpartlemgs2 31748 ballotlemfmpn 31862 isacycgr 32505 isacycgr1 32506 ismfs 32909 dfon2lem3 33143 orderseqlem 33207 frrlem13 33248 elno 33266 elaltxp 33549 bj-ismoore 34520 heiborlem1 35249 heiborlem10 35258 isass 35284 isexid 35285 ismgmOLD 35288 elghomlem2OLD 35324 elcoeleqvrels 35990 eleldisjs 36121 gneispace2 40835 ismnu 40969 nzss 41021 elrnmptf 41807 ismea 43090 isome 43133 ismgmALT 44483 setrec1lem1 45217 |
Copyright terms: Public domain | W3C validator |