Theorem elabg 3614

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 2379. (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 2957	. . . 4 ⊢ Ⅎ𝑥{𝑥 ∣ 𝜑}
2	1	nfel2 2973	. . 3 ⊢ Ⅎ𝑥 𝐴 ∈ {𝑥 ∣ 𝜑}
3		nfv 1915	. . 3 ⊢ Ⅎ𝑥𝜓
4	2, 3	nfbi 1904	. 2 ⊢ Ⅎ𝑥(𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)
5		eleq1 2877	. . 3 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝐴 ∈ {𝑥 ∣ 𝜑}))
6		elabg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
7	5, 6	bibi12d 349	. 2 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑) ↔ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓)))
8		abid 2780	. 2 ⊢ (𝑥 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
9	4, 7, 8	vtoclg1f 3514	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ∈ wcel 2111  {cab 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938

This theorem is referenced by:  elab2g  3616  elabd  3617  intmin3  4866  finds  7589  elfi  8861  inficl  8873  dffi3  8879  scott0  9299  nqpr  10425  hashf1lem1  13809  cshword  14144  trclublem  14346  cotrtrclfv  14363  dfiso2  17034  efgcpbllemb  18873  frgpuplem  18890  lspsn  19767  mpfind  20779  pf1ind  20979  eltg  21562  eltg2  21563  islocfin  22122  fbssfi  22442  isewlk  27392  elabreximd  30278  abfmpunirn  30415  fmlafvel  32745  isfmlasuc  32748  nosupres  33320  nosupbnd1lem3  33323  nosupbnd1lem5  33325  poimirlem3  35060  poimirlem25  35082  islshpkrN  36416  setindtrs  39966  frege55lem1c  40617  nzss  41021  elabrexg  41675  afvelrnb  43719  afvelrnb0  43720  dfatco  43812  elsetpreimafvb  43901  setis  45227