Theorem elabg 3632

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 2372. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2144, ax-11 2160, ax-12 2180. (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 1796	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3627	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 691	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2111  {cab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806

This theorem is referenced by:  elab  3635  elab2g  3636  elabd  3637  elab3g  3641  sbcieg  3781  intmin3  4926  elabrexg  7177  finds  7826  elfi  9297  inficl  9309  dffi3  9315  scott0  9779  elgch  10513  nqpr  10905  hashf1lem1  14362  cshword  14698  trclublem  14902  cotrtrclfv  14919  dfiso2  17679  efgcpbllemb  19668  frgpuplem  19685  lspsn  20936  mpfind  22043  pf1ind  22271  eltg  22873  eltg2  22874  islocfin  23433  fbssfi  23753  nosupres  27647  nosupbnd1lem3  27650  nosupbnd1lem5  27652  noinffv  27661  noinfres  27662  noinfbnd1lem3  27665  noinfbnd1lem5  27667  isewlk  29582  elabreximd  32488  abfmpunirn  32632  ellpi  33336  fmlafvel  35427  isfmlasuc  35430  r1peuqusdeg1  35685  poimirlem3  37669  poimirlem25  37691  islshpkrN  39165  sticksstones8  42192  sticksstones9  42193  sticksstones11  42195  sticksstones17  42202  sticksstones18  42203  rhmqusspan  42224  sn-iotalem  42260  setindtrs  43064  frege55lem1c  43955  nzss  44356  afvelrnb  47200  afvelrnb0  47201  dfatco  47293  elsetpreimafvb  47421  isgrim  47919  isgrlim  48019  discsntermlem  49608  basrestermcfolem  49609  setis  49736