Theorem elabg 3666

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 2390. (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 2979	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	nfel2 2996	. . 3 ⊢ Ⅎ𝑥 𝐴 ∈ {𝑥 ∣ 𝜑}
3		nfv 1915	. . 3 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfbi 1904	. 2 ⊢ Ⅎ𝑥(𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
5		eleq1 2900	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
6		elabg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	bibi12d 348	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) ↔ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)))
8		abid 2803	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	4, 7, 8	vtoclg1f 3566	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ∈ wcel 2114  {cab 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963

This theorem is referenced by:  elab2g  3668  elabd  3669  intmin3  4904  elxpi  5577  finds  7608  elfi  8877  inficl  8889  dffi3  8895  scott0  9315  elgch  10044  nqpr  10436  hashf1lem1  13814  cshword  14153  trclublem  14355  cotrtrclfv  14372  dfiso2  17042  efgcpbllemb  18881  frgpuplem  18898  lspsn  19774  mpfind  20320  pf1ind  20518  eltg  21565  eltg2  21566  islocfin  22125  fbssfi  22445  isewlk  27384  elabreximd  30270  abfmpunirn  30397  fmlafvel  32632  isfmlasuc  32635  nosupres  33207  nosupbnd1lem3  33210  nosupbnd1lem5  33212  poimirlem3  34910  poimirlem25  34932  islshpkrN  36271  setindtrs  39642  frege55lem1c  40282  nzss  40669  elabrexg  41323  afvelrnb  43382  afvelrnb0  43383  dfatco  43475  elsetpreimafvb  43564  setis  44820