Theorem elabg 3620

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 3615	. 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  3623  elab2g  3624  elabd  3625  elab3g  3629  sbcieg  3769  intmin3  4919  elabrexg  7191  finds  7840  elfi  9319  inficl  9331  dffi3  9337  scott0  9801  elgch  10536  nqpr  10928  hashf1lem1  14408  cshword  14744  trclublem  14948  cotrtrclfv  14965  dfiso2  17730  efgcpbllemb  19721  frgpuplem  19738  lspsn  20988  mpfind  22103  pf1ind  22330  eltg  22932  eltg2  22933  islocfin  23492  fbssfi  23812  nosupres  27685  nosupbnd1lem3  27688  nosupbnd1lem5  27690  noinffv  27699  noinfres  27700  noinfbnd1lem3  27703  noinfbnd1lem5  27705  isewlk  29686  elabreximd  32595  abfmpunirn  32740  ellpi  33448  fmlafvel  35583  isfmlasuc  35586  r1peuqusdeg1  35841  poimirlem3  37958  poimirlem25  37980  islshpkrN  39580  sticksstones8  42606  sticksstones9  42607  sticksstones11  42609  sticksstones17  42616  sticksstones18  42617  rhmqusspan  42638  sn-iotalem  42676  setindtrs  43471  frege55lem1c  44361  nzss  44762  afvelrnb  47623  afvelrnb0  47624  dfatco  47716  elsetpreimafvb  47856  isgrim  48370  isgrlim  48470  discsntermlem  50057  basrestermcfolem  50058  setis  50185