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

Theorem elab3 3352
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 3351 . 2 ((𝜓𝐴 ∈ V) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3ax-mp 5 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988  {cab 2606  Vcvv 3195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197
This theorem is referenced by:  fvelrnb  6230  elrnmpt2  6758  ovelrn  6795  isfi  7964  isnum2  8756  pm54.43lem  8810  isfin3  9103  isfin5  9106  isfin6  9107  genpelv  9807  iswrd  13290  4sqlem2  15634  vdwapval  15658  isghm  17641  issrng  18831  lspsnel  18984  lspprel  19075  iscss  20008  ellspd  20122  istps  20719  islp  20925  is2ndc  21230  elpt  21356  itg2l  23477  elply  23932  isismt  25410  isline  34844  ispointN  34847  ispsubsp  34850  ispsubclN  35042  islaut  35188  ispautN  35204  istendo  35867  rngunsnply  37562
  Copyright terms: Public domain W3C validator