Theorem elabg 3646

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 2371. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2142, ax-11 2158, ax-12 2178. (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 1795	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3641	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 691	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804

This theorem is referenced by:  elab  3649  elab2g  3650  elabd  3651  elab3g  3655  sbcieg  3796  intmin3  4943  elabrexg  7220  finds  7875  elfi  9371  inficl  9383  dffi3  9389  scott0  9846  elgch  10582  nqpr  10974  hashf1lem1  14427  cshword  14763  trclublem  14968  cotrtrclfv  14985  dfiso2  17741  efgcpbllemb  19692  frgpuplem  19709  lspsn  20915  mpfind  22021  pf1ind  22249  eltg  22851  eltg2  22852  islocfin  23411  fbssfi  23731  nosupres  27626  nosupbnd1lem3  27629  nosupbnd1lem5  27631  noinffv  27640  noinfres  27641  noinfbnd1lem3  27644  noinfbnd1lem5  27646  isewlk  29537  elabreximd  32446  abfmpunirn  32583  ellpi  33351  fmlafvel  35379  isfmlasuc  35382  r1peuqusdeg1  35637  poimirlem3  37624  poimirlem25  37646  islshpkrN  39120  sticksstones8  42148  sticksstones9  42149  sticksstones11  42151  sticksstones17  42158  sticksstones18  42159  rhmqusspan  42180  sn-iotalem  42216  setindtrs  43021  frege55lem1c  43912  nzss  44313  afvelrnb  47168  afvelrnb0  47169  dfatco  47261  elsetpreimafvb  47389  isgrim  47886  isgrlim  47985  discsntermlem  49563  basrestermcfolem  49564  setis  49691