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

Step	Hyp	Ref	Expression
1		nfab1 2971	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	nfel2 2986	. . 3 ⊢ Ⅎ𝑥 𝐴 ∈ {𝑥 ∣ 𝜑}
3		nfv 2013	. . 3 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfbi 2006	. 2 ⊢ Ⅎ𝑥(𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
5		eleq1 2894	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
6		elabg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	bibi12d 337	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) ↔ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)))
8		abid 2813	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	4, 7, 8	vtoclg1f 3481	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

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