MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elab2g Structured version   Visualization version   GIF version

Theorem elab2g 3665
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2g.1 (𝑥 = 𝐴 → (𝜑𝜓))
elab2g.2 𝐵 = {𝑥𝜑}
Assertion
Ref Expression
elab2g (𝐴𝑉 → (𝐴𝐵𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem elab2g
StepHypRef Expression
1 elab2g.2 . . 3 𝐵 = {𝑥𝜑}
21eleq2i 2901 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 3663 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 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