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

Theorem elab2 3647
Description: Membership in a class abstraction, using implicit substitution. (Contributed by NM, 13-Sep-1995.)
Hypotheses
Ref Expression
elab2.1 𝐴 ∈ V
elab2.2 (𝑥 = 𝐴 → (𝜑𝜓))
elab2.3 𝐵 = {𝑥𝜑}
Assertion
Ref Expression
elab2 (𝐴𝐵𝜓)
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem elab2
StepHypRef Expression
1 elab2.1 . 2 𝐴 ∈ V
2 elab2.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
3 elab2.3 . . 3 𝐵 = {𝑥𝜑}
42, 3elab2g 3645 . 2 (𝐴 ∈ V → (𝐴𝐵𝜓))
51, 4ax-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
This theorem is referenced by:  elpwOLD  4518  elint  4855  opabidw  5385  opabid  5386  elrn2  5794  elimasn  5927  oprabidw  7161  oprabid  7162  wfrlem3a  7932  tfrlem3a  7988  cardprclem  9384  iunfictbso  9517  aceq3lem  9523  dfac5lem4  9529  kmlem9  9561  domtriomlem  9841  ltexprlem3  10437  ltexprlem4  10438  reclem2pr  10447  reclem3pr  10448  supsrlem  10510  supaddc  11585  supadd  11586  supmul1  11587  supmullem1  11588  supmullem2  11589  supmul  11590  sqrlem6  14586  infcvgaux2i  15192  mertenslem1  15219  mertenslem2  15220  4sqlem12  16269  conjnmzb  18372  sylow3lem2  18732  mdetunilem9  21205  txuni2  22149  xkoopn  22173  met2ndci  23108  2sqlem8  25989  2sqlem11  25992  eulerpartlemt  31637  eulerpartlemr  31640  eulerpartlemn  31647  subfacp1lem3  32437  subfacp1lem5  32439  soseq  33104  rdgssun  34679  finxpsuclem  34698  heiborlem1  35131  heiborlem6  35136  heiborlem8  35138  cllem0  40072
  Copyright terms: Public domain W3C validator