Theorem elabg 3633

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 2403. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2178, ax-11 2194, ax-12 2215. (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 1828	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3629	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 704	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2145  {cab 2740

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837

This theorem is used by:  elab  3636  elab2g  3637  elabd  3638  elab3g  3642  sbcieg  3781  intmin3  4939  elabrexg  7244  finds  7897  elfi  9387  inficl  9399  dffi3  9405  scott0b  9880  scott0OLD  9881  elgch  10635  nqpr  11027  hashf1lem1  14524  cshword  14866  trclublem  15072  cotrtrclfv  15089  dfiso2  17867  efgcpbllemb  19888  frgpuplem  19905  lspsn  21192  mpfind  22337  pf1ind  22586  eltg  23188  eltg2  23189  islocfin  23749  fbssfi  24069  nosupres  27951  nosupbnd1lem3  27954  nosupbnd1lem5  27956  noinffv  27965  noinfres  27966  noinfbnd1lem3  27969  noinfbnd1lem5  27971  isewlk  30070  elabreximd  32993  abfmpunirn  33133  ellpi  33815  kardnnfi  35703  rankkardu  35705  fmlafvel  35972  isfmlasuc  35975  r1peuqusdeg1  36230  poimirlem3  38380  poimirlem25  38402  islshpkrN  40001  sticksstones8  43027  sticksstones9  43028  sticksstones11  43030  sticksstones17  43037  sticksstones18  43038  rhmqusspan  43059  sn-iotalem  43099  setindtrs  43874  frege55lem1c  44764  nzss  45149  afvelrnb  48059  afvelrnb0  48060  dfatco  48152  elsetpreimafvb  48292  isgrim  48806  isgrlim  48906  discsntermlem  50504  basrestermcfolem  50505  setis  50632