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

Theorem elab3 3675
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 3674 . 2 ((𝜓𝐴𝑉) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3ax-mp 5 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1533  wcel 2098  {cab 2704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805
This theorem is referenced by:  fvelrnb  6962  elrnmpo  7561  ovelrn  7601  isfi  9001  isnum2  9974  pm54.43lem  10029  isfin3  10325  isfin5  10328  isfin6  10329  genpelv  11029  iswrd  14504  4sqlem2  16923  vdwapval  16947  isghm  19175  issrng  20735  lspsnel  20892  lspprel  20984  iscss  21620  ellspd  21741  istps  22854  islp  23062  is2ndc  23368  elpt  23494  itg2l  25677  elply  26147  isismt  28356  bj-ififc  36063  isline  39216  ispointN  39219  ispsubsp  39222  ispsubclN  39414  islaut  39560  ispautN  39576  istendo  40237  rngunsnply  42600
  Copyright terms: Public domain W3C validator