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

Theorem elab3 3579
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 3578 . 2 ((𝜓𝐴 ∈ V) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3ax-mp 5 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1658  wcel 2166  {cab 2811  Vcvv 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416
This theorem is referenced by:  fvelrnb  6490  elrnmpt2  7033  ovelrn  7070  isfi  8246  isnum2  9084  pm54.43lem  9138  isfin3  9433  isfin5  9436  isfin6  9437  genpelv  10137  iswrd  13576  4sqlem2  16024  vdwapval  16048  isghm  18011  issrng  19206  lspsnel  19362  lspprel  19453  iscss  20390  ellspd  20508  istps  21109  islp  21315  is2ndc  21620  elpt  21746  itg2l  23895  elply  24350  isismt  25846  isline  35814  ispointN  35817  ispsubsp  35820  ispsubclN  36012  islaut  36158  ispautN  36174  istendo  36835  rngunsnply  38586
  Copyright terms: Public domain W3C validator