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

Theorem elab2g 3666
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 2902 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 3664 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 285 1 (𝐴𝑉 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1530  wcel 2107  {cab 2797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961
This theorem is referenced by:  elab2  3668  elab4g  3669  elrab  3678  eldif  3944  elun  4123  elin  4167  elpwg  4543  elsng  4573  elprg  4580  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  7278  elrnmpores  7280  eloprabi  7753  tfrlem12  8017  elqsg  8340  elixp2  8457  isacn  9462  isfin1a  9706  isfin2  9708  isfin4  9711  isfin7  9715  isfin3ds  9743  elwina  10100  elina  10101  iswun  10118  eltskg  10164  elgrug  10206  elnp  10401  elnpi  10402  iscat  16935  isps  17804  isdir  17834  ismgm  17845  elefmndbas2  18031  elsymgbas2  18493  mdetunilem9  21221  istopg  21495  isbasisg  21547  isptfin  22116  isufl  22513  isusp  22862  2sqlem9  25995  isuhgr  26837  isushgr  26838  isupgr  26861  isumgr  26872  isuspgr  26929  isusgr  26930  cplgruvtxb  27187  isconngr  27960  isconngr1  27961  isplig  28245  isgrpo  28266  elunop  29641  adjeu  29658  isarchi  30804  ispcmp  31109  eulerpartlemelr  31603  eulerpartlemgs2  31626  ballotlemfmpn  31740  isacycgr  32380  isacycgr1  32381  ismfs  32784  dfon2lem3  33018  orderseqlem  33082  frrlem13  33123  elno  33141  elaltxp  33424  bj-ismoore  34384  heiborlem1  35076  heiborlem10  35085  isass  35111  isexid  35112  ismgmOLD  35115  elghomlem2OLD  35151  elcoeleqvrels  35817  eleldisjs  35948  gneispace2  40467  ismnu  40582  nzss  40634  elrnmptf  41425  issal  42584  ismea  42718  isome  42761  ismgmALT  44115  setrec1lem1  44775
  Copyright terms: Public domain W3C validator