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

Theorem elab2g 3321
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 2679 . 2 (𝐴𝐵𝐴 ∈ {𝑥𝜑})
3 elab2g.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
43elabg 3319 . 2 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
52, 4syl5bb 270 1 (𝐴𝑉 → (𝐴𝐵𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  {cab 2595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174
This theorem is referenced by:  elab2  3322  elab4g  3323  eldif  3549  elun  3714  elin  3757  elsng  4138  elprg  4143  eluni  4369  elintg  4412  eliun  4454  eliin  4455  elopab  4898  elrn2g  5223  eldmg  5228  elrnmpt  5280  elrnmpt1  5282  elimag  5376  elong  5634  elrnmpt2g  6648  elrnmpt2res  6650  eloprabi  7098  tfrlem12  7349  elqsg  7662  elixp2  7775  isacn  8727  isfin1a  8974  isfin2  8976  isfin4  8979  isfin7  8983  isfin3ds  9011  elwina  9364  elina  9365  iswun  9382  eltskg  9428  elgrug  9470  elnp  9665  elnpi  9666  iscat  16102  isps  16971  isdir  17001  ismgm  17012  elsymgbas2  17570  mdetunilem9  20187  istopg  20467  isbasisg  20504  isptfin  21071  isufl  21469  isusp  21817  2sqlem9  24869  isplig  26486  isgrpo  26501  elunop  27921  adjeu  27938  isarchi  28873  ispcmp  29058  eulerpartlemelr  29552  eulerpartlemgs2  29575  ballotlemfmpn  29689  ismfs  30506  dfon2lem3  30740  orderseqlem  30799  elno  30849  elaltxp  31058  heiborlem1  32583  heiborlem10  32592  isass  32618  isexid  32619  ismgmOLD  32622  elghomlem2OLD  32658  gneispace2  37253  nzss  37341  elrnmptf  38165  issal  39014  isuhgr  40284  isushgr  40285  isupgr  40312  isumgr  40322  isuspgr  40384  isusgr  40385  iscplgr  40638  isconngr  41358  isconngr1  41359  isfrgr  41432  ismgmALT  41651
  Copyright terms: Public domain W3C validator