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

Theorem elab3 3651
Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.)
Hypotheses
Ref Expression
elab3.1 (𝜓𝐴 ∈ V)
elab3.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elab3 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elab3
StepHypRef Expression
1 elab3.1 . 2 (𝜓𝐴 ∈ V)
2 elab3.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32elab3g 3650 . 2 ((𝜓𝐴 ∈ V) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3ax-mp 5 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  wcel 2115  {cab 2799  Vcvv 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-v 3473
This theorem is referenced by:  fvelrnb  6699  elrnmpo  7261  ovelrn  7299  isfi  8508  isnum2  9350  pm54.43lem  9405  isfin3  9695  isfin5  9698  isfin6  9699  genpelv  10399  iswrd  13847  4sqlem2  16262  vdwapval  16286  isghm  18337  issrng  19597  lspsnel  19751  lspprel  19842  iscss  20803  ellspd  20922  istps  21518  islp  21724  is2ndc  22030  elpt  22156  itg2l  24312  elply  24771  isismt  26307  bj-ififc  33923  isline  36917  ispointN  36920  ispsubsp  36923  ispsubclN  37115  islaut  37261  ispautN  37277  istendo  37938  rngunsnply  39924
  Copyright terms: Public domain W3C validator