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

Theorem elabg 3569
 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 2389. (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 2971 . . . 4 𝑥{𝑥𝜑}
21nfel2 2986 . . 3 𝑥 𝐴 ∈ {𝑥𝜑}
3 nfv 2013 . . 3 𝑥𝜓
42, 3nfbi 2006 . 2 𝑥(𝐴 ∈ {𝑥𝜑} ↔ 𝜓)
5 eleq1 2894 . . 3 (𝑥 = 𝐴 → (𝑥 ∈ {𝑥𝜑} ↔ 𝐴 ∈ {𝑥𝜑}))
6 elabg.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
75, 6bibi12d 337 . 2 (𝑥 = 𝐴 → ((𝑥 ∈ {𝑥𝜑} ↔ 𝜑) ↔ (𝐴 ∈ {𝑥𝜑} ↔ 𝜓)))
8 abid 2813 . 2 (𝑥 ∈ {𝑥𝜑} ↔ 𝜑)
94, 7, 8vtoclg1f 3481 1 (𝐴𝑉 → (𝐴 ∈ {𝑥𝜑} ↔ 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   = wceq 1656   ∈ wcel 2164  {cab 2811 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416 This theorem is referenced by:  elab  3571  elab2g  3574  intmin3  4727  elxpi  5368  finds  7358  wfrlem15  7700  elfi  8594  inficl  8606  dffi3  8612  scott0  9033  elgch  9766  nqpr  10158  hashf1lem1  13535  cshword  13917  trclublem  14120  cotrtrclfv  14137  dfiso2  16791  lubval  17344  glbval  17357  efgcpbllemb  18528  frgpuplem  18545  lspsn  19368  mpfind  19903  pf1ind  20086  eltg  21139  eltg2  21140  islocfin  21698  fbssfi  22018  isewlk  26907  elabreximd  29892  abfmpunirn  29997  orvcval  31061  nosupfv  32386  nosupres  32387  nosupbnd1lem3  32390  nosupbnd1lem5  32392  poimirlem3  33955  poimirlem25  33977  islshpkrN  35194  setindtrs  38434  rngunsnply  38585  frege55lem1c  39049  nzss  39355  elabrexg  40023  ismea  41457  afvelrnb  42063  afvelrnb0  42064  dfatco  42156  setis  43353
 Copyright terms: Public domain W3C validator