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

Theorem elab2 3509
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 3508 . 2 (𝐴 ∈ V → (𝐴𝐵𝜓))
51, 4ax-mp 5 1 (𝐴𝐵𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1652  wcel 2155  {cab 2751  Vcvv 3350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352
This theorem is referenced by:  elpw  4321  elint  4639  opabid  5143  elrn2  5534  elimasn  5672  oprabid  6873  wfrlem3a  7620  tfrlem3a  7677  cardprclem  9056  iunfictbso  9188  aceq3lem  9194  dfac5lem4  9200  kmlem9  9233  domtriomlem  9517  ltexprlem3  10113  ltexprlem4  10114  reclem2pr  10123  reclem3pr  10124  supsrlem  10185  supaddc  11244  supadd  11245  supmul1  11246  supmullem1  11247  supmullem2  11248  supmul  11249  sqrlem6  14275  infcvgaux2i  14876  mertenslem1  14901  mertenslem2  14902  4sqlem12  15941  conjnmzb  17961  sylow3lem2  18309  mdetunilem9  20703  txuni2  21648  xkoopn  21672  met2ndci  22606  2sqlem8  25442  2sqlem11  25445  eulerpartlemt  30815  eulerpartlemr  30818  eulerpartlemn  30825  subfacp1lem3  31544  subfacp1lem5  31546  soseq  32130  finxpsuclem  33599  heiborlem1  33964  heiborlem6  33969  heiborlem8  33971  cllem0  38478
  Copyright terms: Public domain W3C validator