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

Theorem elab2 3495
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 3494 . 2 (𝐴 ∈ V → (𝐴𝐵𝜓))
51, 4ax-mp 5 1 (𝐴𝐵𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  wcel 2140  {cab 2747  Vcvv 3341
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 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
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 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343
This theorem is referenced by:  elpw  4309  elint  4634  opabid  5133  elrn2  5521  elimasn  5649  oprabid  6842  wfrlem3a  7588  tfrlem3a  7644  cardprclem  9016  iunfictbso  9148  aceq3lem  9154  dfac5lem4  9160  kmlem9  9193  domtriomlem  9477  ltexprlem3  10073  ltexprlem4  10074  reclem2pr  10083  reclem3pr  10084  supsrlem  10145  supaddc  11203  supadd  11204  supmul1  11205  supmullem1  11206  supmullem2  11207  supmul  11208  sqrlem6  14208  infcvgaux2i  14810  mertenslem1  14836  mertenslem2  14837  4sqlem12  15883  conjnmzb  17917  sylow3lem2  18264  mdetunilem9  20649  txuni2  21591  xkoopn  21615  met2ndci  22549  2sqlem8  25372  2sqlem11  25375  eulerpartlemt  30764  eulerpartlemr  30767  eulerpartlemn  30774  subfacp1lem3  31493  subfacp1lem5  31495  soseq  32082  finxpsuclem  33564  heiborlem1  33942  heiborlem6  33947  heiborlem8  33949  cllem0  38392
  Copyright terms: Public domain W3C validator