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

Theorem elab3 3673
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 3672 . 2 ((𝜓𝐴𝑉) → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
41, 3ax-mp 5 1 (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  wcel 2099  {cab 2704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805
This theorem is referenced by:  fvelrnb  6953  elrnmpo  7551  ovelrn  7591  isfi  8988  isnum2  9960  pm54.43lem  10015  isfin3  10311  isfin5  10314  isfin6  10315  genpelv  11015  iswrd  14490  4sqlem2  16909  vdwapval  16933  isghm  19161  issrng  20719  lspsnel  20876  lspprel  20968  iscss  21602  ellspd  21723  istps  22823  islp  23031  is2ndc  23337  elpt  23463  itg2l  25646  elply  26116  isismt  28325  bj-ififc  35994  isline  39149  ispointN  39152  ispsubsp  39155  ispsubclN  39347  islaut  39493  ispautN  39509  istendo  40170  rngunsnply  42519
  Copyright terms: Public domain W3C validator