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

Theorem elab2 3322
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 3321 . 2 (𝐴 ∈ V → (𝐴𝐵𝜓))
51, 4ax-mp 5 1 (𝐴𝐵𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  {cab 2595  Vcvv 3172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174
This theorem is referenced by:  elpw  4113  elint  4410  opabid  4897  elrn2  5273  elimasn  5396  oprabid  6554  wfrlem3a  7281  tfrlem3a  7337  cardprclem  8665  iunfictbso  8797  aceq3lem  8803  dfac5lem4  8809  kmlem9  8840  domtriomlem  9124  ltexprlem3  9716  ltexprlem4  9717  reclem2pr  9726  reclem3pr  9727  supsrlem  9788  supaddc  10837  supadd  10838  supmul1  10839  supmullem1  10840  supmullem2  10841  supmul  10842  sqrlem6  13782  infcvgaux2i  14375  mertenslem1  14401  mertenslem2  14402  4sqlem12  15444  conjnmzb  17464  sylow3lem2  17812  mdetunilem9  20187  txuni2  21120  xkoopn  21144  met2ndci  22078  2sqlem8  24868  2sqlem11  24871  eulerpartlemt  29566  eulerpartlemr  29569  eulerpartlemn  29576  subfacp1lem3  30224  subfacp1lem5  30226  soseq  30801  nofulllem5  30911  finxpsuclem  32213  heiborlem1  32583  heiborlem6  32588  heiborlem8  32590  cllem0  36693
  Copyright terms: Public domain W3C validator