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  14381  cshword  14716  trclublem  14921  cotrtrclfv  14938  dfiso2  17698  efgcpbllemb  19653  frgpuplem  19670  lspsn  20924  mpfind  22031  pf1ind  22259  eltg  22861  eltg2  22862  islocfin  23421  fbssfi  23741  nosupres  27636  nosupbnd1lem3  27639  nosupbnd1lem5  27641  noinffv  27650  noinfres  27651  noinfbnd1lem3  27654  noinfbnd1lem5  27656  isewlk  29567  elabreximd  32473  abfmpunirn  32614  ellpi  33329  fmlafvel  35377  isfmlasuc  35380  r1peuqusdeg1  35635  poimirlem3  37622  poimirlem25  37644  islshpkrN  39118  sticksstones8  42146  sticksstones9  42147  sticksstones11  42149  sticksstones17  42156  sticksstones18  42157  rhmqusspan  42178  sn-iotalem  42214  setindtrs  43018  frege55lem1c  43909  nzss  44310  afvelrnb  47167  afvelrnb0  47168  dfatco  47260  elsetpreimafvb  47388  isgrim  47886  isgrlim  47986  discsntermlem  49575  basrestermcfolem  49576  setis  49703