Theorem elabg 3630

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836

This theorem is used by:  elab  3633  elab2g  3634  elabd  3635  elab3g  3639  sbcieg  3778  intmin3  4936  elabrexg  7239  finds  7897  elfi  9389  inficl  9401  dffi3  9407  scott0b  9918  scott0OLD  9919  elgch  10688  nqpr  11080  hashf1lem1  14580  cshword  14922  trclublem  15128  cotrtrclfv  15145  dfiso2  17927  efgcpbllemb  19949  frgpuplem  19966  lspsn  21257  mpfind  22404  pf1ind  22653  eltg  23255  eltg2  23256  islocfin  23816  fbssfi  24136  nosupres  28046  nosupbnd1lem3  28049  nosupbnd1lem5  28051  noinffv  28060  noinfres  28061  noinfbnd1lem3  28064  noinfbnd1lem5  28066  isewlk  30165  elabreximd  33088  abfmpunirn  33228  ellpi  33910  kardnnfi  35810  rankkardu  35812  fmlafvel  36119  isfmlasuc  36122  r1peuqusdeg1  36377  poimirlem3  38509  poimirlem25  38531  islshpkrN  40145  sticksstones8  43171  sticksstones9  43172  sticksstones11  43174  sticksstones17  43181  sticksstones18  43182  rhmqusspan  43203  sn-iotalem  43243  setindtrs  43985  frege55lem1c  44875  nzss  45260  afvelrnb  48177  afvelrnb0  48178  dfatco  48270  elsetpreimafvb  48410  isgrim  48924  isgrlim  49024  discsntermlem  50622  basrestermcfolem  50623  setis  50735