New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  elab2g GIF version

Theorem elab2g 2987
 Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2g.1 (x = A → (φψ))
elab2g.2 B = {x φ}
Assertion
Ref Expression
elab2g (A V → (A Bψ))
Distinct variable groups:   ψ,x   x,A
Allowed substitution hints:   φ(x)   B(x)   V(x)

Proof of Theorem elab2g
StepHypRef Expression
1 elab2g.2 . . 3 B = {x φ}
21eleq2i 2417 . 2 (A BA {x φ})
3 elab2g.1 . . 3 (x = A → (φψ))
43elabg 2986 . 2 (A V → (A {x φ} ↔ ψ))
52, 4syl5bb 248 1 (A V → (A Bψ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710  {cab 2339 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861 This theorem is referenced by:  elab2  2988  elab4g  2989  elning  3217  elprg  3750  elsncg  3755  eluni  3894  eliun  3973  eliin  3974  el1c  4139  elxpk  4196  elimakg  4257  elp6  4263  eladdc  4398  evennn  4506  oddnn  4507  evennnul  4508  oddnnul  4509  sucevenodd  4510  sucoddeven  4511  eventfin  4517  oddtfin  4518  elopab  4696  elima  4754  opeliunxp  4820  elqsg  5976  elcan  6329  elscan  6330
 Copyright terms: Public domain W3C validator