Theorem elabg 3638

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 2407. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2179, ax-11 2195, ax-12 2216. (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 1828	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3634	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 704	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2146  {cab 2744

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841

This theorem is used by:  elab  3641  elab2g  3642  elabd  3643  elab3g  3647  sbcieg  3786  intmin3  4946  elabrexg  7248  finds  7902  elfi  9383  inficl  9395  dffi3  9401  scott0b  9876  scott0OLD  9877  elgch  10625  nqpr  11017  hashf1lem1  14512  cshword  14854  trclublem  15058  cotrtrclfv  15075  dfiso2  17854  efgcpbllemb  19856  frgpuplem  19873  lspsn  21160  mpfind  22303  pf1ind  22552  eltg  23151  eltg2  23152  islocfin  23711  fbssfi  24031  nosupres  27908  nosupbnd1lem3  27911  nosupbnd1lem5  27913  noinffv  27922  noinfres  27923  noinfbnd1lem3  27926  noinfbnd1lem5  27928  isewlk  29989  elabreximd  32893  abfmpunirn  33034  ellpi  33718  kardnnfi  35606  rankkardu  35608  fmlafvel  35898  isfmlasuc  35901  r1peuqusdeg1  36156  poimirlem3  38315  poimirlem25  38337  islshpkrN  39935  sticksstones8  42961  sticksstones9  42962  sticksstones11  42964  sticksstones17  42971  sticksstones18  42972  rhmqusspan  42993  sn-iotalem  43033  setindtrs  43793  frege55lem1c  44683  nzss  45068  afvelrnb  47941  afvelrnb0  47942  dfatco  48034  elsetpreimafvb  48174  isgrim  48688  isgrlim  48788  discsntermlem  50389  basrestermcfolem  50390  setis  50517