Theorem elabg 3634

Description: Membership in a class abstraction, using implicit substitution. Compare Theorem 6.13 of [Quine] p. 44. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2370. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (Revised by SN, 5-Oct-2024.)

Hypothesis

Ref	Expression
elabg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elabg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴

Allowed substitution hints:   𝜑(𝑥)   𝑉(𝑥)

Proof of Theorem elabg

Step	Hyp	Ref	Expression
1		elabg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
2	1	ax-gen 1795	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3629	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 691	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elab  3637  elab2g  3638  elabd  3639  elab3g  3643  sbcieg  3784  intmin3  4929  elabrexg  7183  finds  7836  elfi  9322  inficl  9334  dffi3  9340  scott0  9801  elgch  10535  nqpr  10927  hashf1lem1  14380  cshword  14715  trclublem  14920  cotrtrclfv  14937  dfiso2  17697  efgcpbllemb  19652  frgpuplem  19669  lspsn  20923  mpfind  22030  pf1ind  22258  eltg  22860  eltg2  22861  islocfin  23420  fbssfi  23740  nosupres  27635  nosupbnd1lem3  27638  nosupbnd1lem5  27640  noinffv  27649  noinfres  27650  noinfbnd1lem3  27653  noinfbnd1lem5  27655  isewlk  29566  elabreximd  32472  abfmpunirn  32609  ellpi  33320  fmlafvel  35357  isfmlasuc  35360  r1peuqusdeg1  35615  poimirlem3  37602  poimirlem25  37624  islshpkrN  39098  sticksstones8  42126  sticksstones9  42127  sticksstones11  42129  sticksstones17  42136  sticksstones18  42137  rhmqusspan  42158  sn-iotalem  42194  setindtrs  42998  frege55lem1c  43889  nzss  44290  afvelrnb  47148  afvelrnb0  47149  dfatco  47241  elsetpreimafvb  47369  isgrim  47867  isgrlim  47967  discsntermlem  49556  basrestermcfolem  49557  setis  49684