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 2404. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2180, ax-11 2197, 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 3629	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 704	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839

This theorem is used by:  elab  3636  elab2g  3637  elabd  3638  elab3g  3642  sbcieg  3781  intmin3  4939  elabrexg  7273  finds  7935  elfi  9435  inficl  9447  dffi3  9453  scott0b  9967  scott0OLD  9968  elgch  10737  nqpr  11129  hashf1lem1  14630  cshword  14973  trclublem  15180  cotrtrclfv  15197  dfiso2  17979  efgcpbllemb  20002  frgpuplem  20019  lspsn  21310  mpfind  22457  pf1ind  22706  eltg  23308  eltg2  23309  islocfin  23869  fbssfi  24189  nosupres  28097  nosupbnd1lem3  28100  nosupbnd1lem5  28102  noinffv  28111  noinfres  28112  noinfbnd1lem3  28115  noinfbnd1lem5  28117  isewlk  30216  elabreximd  33181  abfmpunirn  33321  ellpi  34012  kardnnfi  35950  rankkardu  35952  fmlafvel  36330  isfmlasuc  36333  r1peuqusdeg1  36588  poimirlem3  38746  poimirlem25  38768  islshpkrN  40380  sticksstones8  43406  sticksstones9  43407  sticksstones11  43409  sticksstones17  43416  sticksstones18  43417  rhmqusspan  43438  sn-iotalem  43479  setindtrs  44236  frege55lem1c  45119  nzss  45504  afvelrnb  48448  afvelrnb0  48449  dfatco  48541  elsetpreimafvb  48681  isgrim  49195  isgrlim  49295  discsntermlem  50923  basrestermcfolem  50924  setis  51081