Theorem elabg 3642

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 2410. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2182, ax-11 2198, ax-12 2219. (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 1822	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3638	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 703	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565   = wceq 1567   ∈ wcel 2149  {cab 2747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844

This theorem is referenced by:  elab  3645  elab2g  3646  elabd  3647  elab3g  3651  sbcieg  3790  intmin3  4943  elabrexg  7242  finds  7893  elfi  9373  inficl  9385  dffi3  9391  scott0  9860  elgch  10607  nqpr  10999  hashf1lem1  14492  cshword  14828  trclublem  15032  cotrtrclfv  15049  dfiso2  17829  efgcpbllemb  19825  frgpuplem  19842  lspsn  21101  mpfind  22235  pf1ind  22484  eltg  23083  eltg2  23084  islocfin  23643  fbssfi  23963  nosupres  27837  nosupbnd1lem3  27840  nosupbnd1lem5  27842  noinffv  27851  noinfres  27852  noinfbnd1lem3  27855  noinfbnd1lem5  27857  isewlk  29893  elabreximd  32797  abfmpunirn  32938  ellpi  33630  kardnnfi  35515  rankkardu  35517  fmlafvel  35810  isfmlasuc  35813  r1peuqusdeg1  36068  poimirlem3  38197  poimirlem25  38219  islshpkrN  39819  sticksstones8  42845  sticksstones9  42846  sticksstones11  42848  sticksstones17  42855  sticksstones18  42856  rhmqusspan  42877  sn-iotalem  42917  setindtrs  43679  frege55lem1c  44569  nzss  44954  afvelrnb  47824  afvelrnb0  47825  dfatco  47917  elsetpreimafvb  48057  isgrim  48571  isgrlim  48671  discsntermlem  50268  basrestermcfolem  50269  setis  50396