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

Theorem elab3 3686
Description: Membership in a class abstraction using implicit substitution. (Contributed by NM, 10-Nov-2000.) (Revised by AV, 16-Aug-2024.)
Hypotheses
Ref Expression
elab3.1 (𝜓𝐴𝑉)
elab3.2 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elab3 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elab3
StepHypRef Expression
1 elab3.1 . 2 (𝜓𝐴𝑉)
2 elab3.2 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
32elab3g 3685 . 2 ((𝜓𝐴𝑉) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3ax-mp 5 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  {cab 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816
This theorem is referenced by:  fvelrnb  6969  elrnmpo  7569  ovelrn  7609  isfi  9016  isnum2  9985  pm54.43lem  10040  isfin3  10336  isfin5  10339  isfin6  10340  genpelv  11040  iswrd  14554  4sqlem2  16987  vdwapval  17011  isghm  19233  isghmOLD  19234  issrng  20845  ellspsn  21001  lspprel  21093  iscss  21701  ellspd  21822  istps  22940  islp  23148  is2ndc  23454  elpt  23580  itg2l  25764  elply  26234  isismt  28542  bj-ififc  36583  isline  39741  ispointN  39744  ispsubsp  39747  ispsubclN  39939  islaut  40085  ispautN  40101  istendo  40762  sn-isghm  42683  rngunsnply  43181
  Copyright terms: Public domain W3C validator