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

Theorem elab2 3494
 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 3493 . 2 (𝐴 ∈ V → (𝐴𝐵𝜓))
51, 4ax-mp 5 1 (𝐴𝐵𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632   ∈ wcel 2139  {cab 2746  Vcvv 3340 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342 This theorem is referenced by:  elpw  4308  elint  4633  opabid  5132  elrn2  5520  elimasn  5648  oprabid  6840  wfrlem3a  7586  tfrlem3a  7642  cardprclem  8995  iunfictbso  9127  aceq3lem  9133  dfac5lem4  9139  kmlem9  9172  domtriomlem  9456  ltexprlem3  10052  ltexprlem4  10053  reclem2pr  10062  reclem3pr  10063  supsrlem  10124  supaddc  11182  supadd  11183  supmul1  11184  supmullem1  11185  supmullem2  11186  supmul  11187  sqrlem6  14187  infcvgaux2i  14789  mertenslem1  14815  mertenslem2  14816  4sqlem12  15862  conjnmzb  17896  sylow3lem2  18243  mdetunilem9  20628  txuni2  21570  xkoopn  21594  met2ndci  22528  2sqlem8  25350  2sqlem11  25353  eulerpartlemt  30742  eulerpartlemr  30745  eulerpartlemn  30752  subfacp1lem3  31471  subfacp1lem5  31473  soseq  32060  finxpsuclem  33545  heiborlem1  33923  heiborlem6  33928  heiborlem8  33930  cllem0  38373
 Copyright terms: Public domain W3C validator