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

Theorem elab2g 3505
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 2842 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 3503 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 272 1 (𝐴𝑉 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145  {cab 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353
This theorem is referenced by:  elab2  3506  elab4g  3507  eldif  3734  elun  3905  elin  3948  elsng  4331  elprg  4337  eluni  4578  elintg  4620  eliun  4659  eliin  4660  elopab  5117  elrn2g  5452  eldmg  5458  elrnmpt  5511  elrnmpt1  5513  elimag  5612  elong  5875  elrnmpt2g  6920  elrnmpt2res  6922  eloprabi  7383  tfrlem12  7639  elqsg  7951  elixp2  8067  isacn  9068  isfin1a  9317  isfin2  9319  isfin4  9322  isfin7  9326  isfin3ds  9354  elwina  9711  elina  9712  iswun  9729  eltskg  9775  elgrug  9817  elnp  10012  elnpi  10013  iscat  16541  isps  17411  isdir  17441  ismgm  17452  elsymgbas2  18009  mdetunilem9  20645  istopg  20921  isbasisg  20973  isptfin  21541  isufl  21938  isusp  22286  2sqlem9  25374  isuhgr  26177  isushgr  26178  isupgr  26201  isumgr  26212  isuspgr  26270  isusgr  26271  cplgruvtxb  26544  isconngr  27370  isconngr1  27371  isfrgr  27441  isplig  27671  isgrpo  27692  elunop  29072  adjeu  29089  isarchi  30077  ispcmp  30265  eulerpartlemelr  30760  eulerpartlemgs2  30783  ballotlemfmpn  30897  ismfs  31785  dfon2lem3  32027  orderseqlem  32090  elno  32137  elaltxp  32420  bj-ismoore  33392  heiborlem1  33943  heiborlem10  33952  isass  33978  isexid  33979  ismgmOLD  33982  elghomlem2OLD  34018  gneispace2  38957  nzss  39043  elrnmptf  39888  issal  41052  isome  41229  ismgmALT  42388  setrec1lem1  42963
  Copyright terms: Public domain W3C validator