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 2901 | . 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}) |
3 | elab2g.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 3 | elabg 3663 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)) |
5 | 2, 4 | syl5bb 284 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ∈ wcel 2105 {cab 2796 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 |
This theorem is referenced by: elab2 3667 elab4g 3668 elrab 3677 eldif 3943 elun 4122 elin 4166 elpwg 4541 elsng 4571 elprg 4578 eluni 4833 elintg 4875 eliun 4914 eliin 4915 elopab 5405 elrn2g 5754 eldmg 5760 dmopabelb 5778 elrnmpt 5821 elrnmpt1 5823 elimag 5926 elong 6192 elrnmpog 7275 elrnmpores 7277 eloprabi 7750 tfrlem12 8014 elqsg 8337 elixp2 8453 isacn 9458 isfin1a 9702 isfin2 9704 isfin4 9707 isfin7 9711 isfin3ds 9739 elwina 10096 elina 10097 iswun 10114 eltskg 10160 elgrug 10202 elnp 10397 elnpi 10398 iscat 16931 isps 17800 isdir 17830 ismgm 17841 elsymgbas2 18437 mdetunilem9 21157 istopg 21431 isbasisg 21483 isptfin 22052 isufl 22449 isusp 22797 2sqlem9 25930 isuhgr 26772 isushgr 26773 isupgr 26796 isumgr 26807 isuspgr 26864 isusgr 26865 cplgruvtxb 27122 isconngr 27895 isconngr1 27896 isplig 28180 isgrpo 28201 elunop 29576 adjeu 29593 isarchi 30738 ispcmp 31020 eulerpartlemelr 31514 eulerpartlemgs2 31537 ballotlemfmpn 31651 isacycgr 32289 isacycgr1 32290 ismfs 32693 dfon2lem3 32927 orderseqlem 32991 frrlem13 33032 elno 33050 elaltxp 33333 bj-ismoore 34291 heiborlem1 34970 heiborlem10 34979 isass 35005 isexid 35006 ismgmOLD 35009 elghomlem2OLD 35045 elcoeleqvrels 35710 eleldisjs 35841 gneispace2 40360 ismnu 40474 nzss 40526 elrnmptf 41317 issal 42476 ismea 42610 isome 42653 ismgmALT 44058 setrec1lem1 44718 |
Copyright terms: Public domain | W3C validator |