Theorem elabg 3629

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 2401. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2177, ax-11 2193, ax-12 2212. (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 1827	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3625	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 704	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569   ∈ wcel 2144  {cab 2738

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835

This theorem is used by:  elab  3632  elab2g  3633  elabd  3634  elab3g  3638  sbcieg  3777  intmin3  4935  elabrexg  7248  finds  7909  elfi  9409  inficl  9421  dffi3  9427  scott0b  9941  scott0OLD  9942  elgch  10711  nqpr  11103  hashf1lem1  14604  cshword  14947  trclublem  15154  cotrtrclfv  15171  dfiso2  17953  efgcpbllemb  19975  frgpuplem  19992  lspsn  21283  mpfind  22430  pf1ind  22679  eltg  23281  eltg2  23282  islocfin  23842  fbssfi  24162  nosupres  28070  nosupbnd1lem3  28073  nosupbnd1lem5  28075  noinffv  28084  noinfres  28085  noinfbnd1lem3  28088  noinfbnd1lem5  28090  isewlk  30189  elabreximd  33154  abfmpunirn  33294  ellpi  33975  kardnnfi  35894  rankkardu  35896  fmlafvel  36237  isfmlasuc  36240  r1peuqusdeg1  36495  poimirlem3  38635  poimirlem25  38657  islshpkrN  40271  sticksstones8  43297  sticksstones9  43298  sticksstones11  43300  sticksstones17  43307  sticksstones18  43308  rhmqusspan  43329  sn-iotalem  43369  setindtrs  44126  frege55lem1c  45010  nzss  45395  afvelrnb  48327  afvelrnb0  48328  dfatco  48420  elsetpreimafvb  48560  isgrim  49074  isgrlim  49174  discsntermlem  50802  basrestermcfolem  50803  setis  50960