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

Theorem elab2g 3493
 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 2831 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 3491 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 272 1 (𝐴𝑉 → (𝐴𝐵𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2139  {cab 2746 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342 This theorem is referenced by:  elab2  3494  elab4g  3495  eldif  3725  elun  3896  elin  3939  elsng  4335  elprg  4341  eluni  4591  elintg  4635  eliun  4676  eliin  4677  elopab  5133  elrn2g  5468  eldmg  5474  elrnmpt  5527  elrnmpt1  5529  elimag  5628  elong  5892  elrnmpt2g  6938  elrnmpt2res  6940  eloprabi  7401  tfrlem12  7655  elqsg  7967  elixp2  8080  isacn  9077  isfin1a  9326  isfin2  9328  isfin4  9331  isfin7  9335  isfin3ds  9363  elwina  9720  elina  9721  iswun  9738  eltskg  9784  elgrug  9826  elnp  10021  elnpi  10022  iscat  16554  isps  17423  isdir  17453  ismgm  17464  elsymgbas2  18021  mdetunilem9  20648  istopg  20922  isbasisg  20973  isptfin  21541  isufl  21938  isusp  22286  2sqlem9  25372  isuhgr  26175  isushgr  26176  isupgr  26199  isumgr  26210  isuspgr  26267  isusgr  26268  cplgruvtxb  26539  isconngr  27362  isconngr1  27363  isfrgr  27433  isplig  27660  isgrpo  27681  elunop  29061  adjeu  29078  isarchi  30066  ispcmp  30254  eulerpartlemelr  30749  eulerpartlemgs2  30772  ballotlemfmpn  30886  ismfs  31774  dfon2lem3  32016  orderseqlem  32079  elno  32126  elaltxp  32409  bj-ismoore  33383  heiborlem1  33941  heiborlem10  33950  isass  33976  isexid  33977  ismgmOLD  33980  elghomlem2OLD  34016  gneispace2  38950  nzss  39036  elrnmptf  39884  issal  41055  isome  41232  ismgmALT  42387  setrec1lem1  42962
 Copyright terms: Public domain W3C validator