Theorem elabg 3633

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 2377. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2147, ax-11 2163, ax-12 2185. (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 1797	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3628	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 692	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540   = wceq 1542   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812

This theorem is referenced by:  elab  3636  elab2g  3637  elabd  3638  elab3g  3642  sbcieg  3782  intmin3  4933  elabrexg  7199  finds  7848  elfi  9328  inficl  9340  dffi3  9346  scott0  9810  elgch  10545  nqpr  10937  hashf1lem1  14390  cshword  14726  trclublem  14930  cotrtrclfv  14947  dfiso2  17708  efgcpbllemb  19696  frgpuplem  19713  lspsn  20965  mpfind  22082  pf1ind  22311  eltg  22913  eltg2  22914  islocfin  23473  fbssfi  23793  nosupres  27687  nosupbnd1lem3  27690  nosupbnd1lem5  27692  noinffv  27701  noinfres  27702  noinfbnd1lem3  27705  noinfbnd1lem5  27707  isewlk  29688  elabreximd  32596  abfmpunirn  32741  ellpi  33465  fmlafvel  35598  isfmlasuc  35601  r1peuqusdeg1  35856  poimirlem3  37871  poimirlem25  37893  islshpkrN  39493  sticksstones8  42520  sticksstones9  42521  sticksstones11  42523  sticksstones17  42530  sticksstones18  42531  rhmqusspan  42552  sn-iotalem  42590  setindtrs  43379  frege55lem1c  44269  nzss  44670  afvelrnb  47520  afvelrnb0  47521  dfatco  47613  elsetpreimafvb  47741  isgrim  48239  isgrlim  48339  discsntermlem  49926  basrestermcfolem  49927  setis  50054