Theorem elabg 3636

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 2404. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2176, ax-11 2192, ax-12 2213. (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 1825	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3632	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 703	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838

This theorem is referenced by:  elab  3639  elab2g  3640  elabd  3641  elab3g  3645  sbcieg  3784  intmin3  4942  elabrexg  7243  finds  7894  elfi  9374  inficl  9386  dffi3  9392  scott0  9861  elgch  10608  nqpr  11000  hashf1lem1  14494  cshword  14830  trclublem  15034  cotrtrclfv  15051  dfiso2  17830  efgcpbllemb  19826  frgpuplem  19843  lspsn  21104  mpfind  22247  pf1ind  22496  eltg  23095  eltg2  23096  islocfin  23655  fbssfi  23975  nosupres  27852  nosupbnd1lem3  27855  nosupbnd1lem5  27857  noinffv  27866  noinfres  27867  noinfbnd1lem3  27870  noinfbnd1lem5  27872  isewlk  29933  elabreximd  32837  abfmpunirn  32978  ellpi  33668  kardnnfi  35563  rankkardu  35565  fmlafvel  35858  isfmlasuc  35861  r1peuqusdeg1  36116  poimirlem3  38255  poimirlem25  38277  islshpkrN  39875  sticksstones8  42901  sticksstones9  42902  sticksstones11  42904  sticksstones17  42911  sticksstones18  42912  rhmqusspan  42933  sn-iotalem  42973  setindtrs  43735  frege55lem1c  44625  nzss  45010  afvelrnb  47883  afvelrnb0  47884  dfatco  47976  elsetpreimafvb  48116  isgrim  48630  isgrlim  48730  discsntermlem  50331  basrestermcfolem  50332  setis  50459