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

Theorem elab2g 3226
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 2584 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 3224 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 270 1 (𝐴𝑉 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1938  {cab 2500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-v 3079
This theorem is referenced by:  elab2  3227  elab4g  3228  eldif  3454  elun  3619  elin  3662  elsng  4042  elprg  4047  eluni  4273  elintg  4316  eliun  4358  eliin  4359  elopab  4802  elrn2g  5127  eldmg  5132  elrnmpt  5184  elrnmpt1  5186  elimag  5279  elong  5538  elrnmpt2g  6546  elrnmpt2res  6548  eloprabi  6995  tfrlem12  7247  elqsg  7560  elixp2  7673  isacn  8625  isfin1a  8872  isfin2  8874  isfin4  8877  isfin7  8881  isfin3ds  8909  elwina  9262  elina  9263  iswun  9280  eltskg  9326  elgrug  9368  elnp  9563  elnpi  9564  iscat  16046  isps  16915  isdir  16945  ismgm  16956  elsymgbas2  17514  mdetunilem9  20146  istopg  20426  isbasisg  20463  isptfin  21030  isufl  21428  isusp  21776  2sqlem9  24842  isplig  26459  isgrpo  26474  elunop  27904  adjeu  27921  isarchi  28864  ispcmp  29049  eulerpartlemelr  29554  eulerpartlemgs2  29577  ballotlemfmpn  29691  ismfs  30546  dfon2lem3  30777  orderseqlem  30836  elno  30879  elaltxp  31088  heiborlem1  32655  heiborlem10  32664  isass  32690  isexid  32691  ismgmOLD  32694  elghomlem2OLD  32730  gneispace2  37332  nzss  37420  elrnmptf  38245  issal  39104  isuhgr  40374  isushgr  40375  isupgr  40402  isumgr  40412  isuspgr  40474  isusgr  40475  iscplgr  40728  isconngr  41448  isconngr1  41449  isfrgr  41522  ismgmALT  41741
  Copyright terms: Public domain W3C validator