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

Theorem elabg 3665
Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) Remove dependency on ax-13 2386. (Revised by Steven Nguyen, 23-Nov-2022.)
Hypothesis
Ref Expression
elabg.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elabg (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴
Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elabg
StepHypRef Expression
1 nfab1 2979 . . . 4 𝑥{𝑥𝜑}
21nfel2 2996 . . 3 𝑥 𝐴 ∈ {𝑥𝜑}
3 nfv 1911 . . 3 𝑥𝜓
42, 3nfbi 1900 . 2 𝑥(𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
5 eleq1 2900 . . 3 (𝑥 = 𝐴 → (𝑥 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
6 elabg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6bibi12d 348 . 2 (𝑥 = 𝐴 → ((𝑥 ∈ {𝑥𝜑} ↔ 𝜑) ↔ (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)))
8 abid 2803 . 2 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
94, 7, 8vtoclg1f 3566 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208   = wceq 1533  wcel 2110  {cab 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963
This theorem is referenced by:  elab2g  3667  elabd  3668  intmin3  4903  elxpi  5576  finds  7607  elfi  8876  inficl  8888  dffi3  8894  scott0  9314  elgch  10043  nqpr  10435  hashf1lem1  13812  cshword  14152  trclublem  14354  cotrtrclfv  14371  dfiso2  17041  efgcpbllemb  18880  frgpuplem  18897  lspsn  19773  mpfind  20319  pf1ind  20517  eltg  21564  eltg2  21565  islocfin  22124  fbssfi  22444  isewlk  27383  elabreximd  30269  abfmpunirn  30396  fmlafvel  32632  isfmlasuc  32635  nosupres  33207  nosupbnd1lem3  33210  nosupbnd1lem5  33212  poimirlem3  34894  poimirlem25  34916  islshpkrN  36255  setindtrs  39620  frege55lem1c  40260  nzss  40647  elabrexg  41301  afvelrnb  43361  afvelrnb0  43362  dfatco  43454  elsetpreimafvb  43543  setis  44799
  Copyright terms: Public domain W3C validator