Theorem elabg 3621

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 2380. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2152, ax-11 2168, ax-12 2189. (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 1802	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3617	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 697	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1545   = wceq 1547   ∈ wcel 2119  {cab 2718

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815

This theorem is referenced by:  elab  3624  elab2g  3625  elabd  3626  elab3g  3630  sbcieg  3769  intmin3  4913  elabrexg  7194  finds  7843  elfi  9323  inficl  9335  dffi3  9341  scott0  9808  elgch  10543  nqpr  10935  hashf1lem1  14415  cshword  14751  trclublem  14955  cotrtrclfv  14972  dfiso2  17737  efgcpbllemb  19728  frgpuplem  19745  lspsn  20999  mpfind  22098  pf1ind  22348  eltg  22947  eltg2  22948  islocfin  23507  fbssfi  23827  nosupres  27696  nosupbnd1lem3  27699  nosupbnd1lem5  27701  noinffv  27710  noinfres  27711  noinfbnd1lem3  27714  noinfbnd1lem5  27716  isewlk  29696  elabreximd  32605  abfmpunirn  32751  ellpi  33463  fmlafvel  35620  isfmlasuc  35623  r1peuqusdeg1  35878  poimirlem3  37997  poimirlem25  38019  islshpkrN  39619  sticksstones8  42645  sticksstones9  42646  sticksstones11  42648  sticksstones17  42655  sticksstones18  42656  rhmqusspan  42677  sn-iotalem  42715  setindtrs  43477  frege55lem1c  44367  nzss  44768  afvelrnb  47633  afvelrnb0  47634  dfatco  47726  elsetpreimafvb  47866  isgrim  48380  isgrlim  48480  discsntermlem  50067  basrestermcfolem  50068  setis  50195