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 2402. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2174, ax-11 2190, ax-12 2211. (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 1814	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3630	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 701	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   = wceq 1559   ∈ wcel 2141  {cab 2739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is referenced by:  elab  3637  elab2g  3638  elabd  3639  elab3g  3643  sbcieg  3781  intmin3  4931  elabrexg  7221  finds  7871  elfi  9352  inficl  9364  dffi3  9370  scott0  9837  elgch  10573  nqpr  10965  hashf1lem1  14461  cshword  14797  trclublem  15001  cotrtrclfv  15018  dfiso2  17795  efgcpbllemb  19785  frgpuplem  19802  lspsn  21056  mpfind  22155  pf1ind  22405  eltg  23004  eltg2  23005  islocfin  23564  fbssfi  23884  nosupres  27758  nosupbnd1lem3  27761  nosupbnd1lem5  27763  noinffv  27772  noinfres  27773  noinfbnd1lem3  27776  noinfbnd1lem5  27778  isewlk  29759  elabreximd  32668  abfmpunirn  32814  ellpi  33519  fmlafvel  35695  isfmlasuc  35698  r1peuqusdeg1  35953  poimirlem3  38082  poimirlem25  38104  islshpkrN  39704  sticksstones8  42730  sticksstones9  42731  sticksstones11  42733  sticksstones17  42740  sticksstones18  42741  rhmqusspan  42762  sn-iotalem  42800  setindtrs  43562  frege55lem1c  44452  nzss  44853  afvelrnb  47717  afvelrnb0  47718  dfatco  47810  elsetpreimafvb  47950  isgrim  48464  isgrlim  48564  discsntermlem  50151  basrestermcfolem  50152  setis  50279