Theorem elabg 3631

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 2376. (Revised by SN, 23-Nov-2022.) Avoid ax-10 2146, ax-11 2162, ax-12 2184. (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 1796	. 2 ⊢ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
3		elabgt 3626	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 691	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1539   = wceq 1541   ∈ wcel 2113  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elab  3634  elab2g  3635  elabd  3636  elab3g  3640  sbcieg  3780  intmin3  4931  elabrexg  7189  finds  7838  elfi  9316  inficl  9328  dffi3  9334  scott0  9798  elgch  10533  nqpr  10925  hashf1lem1  14378  cshword  14714  trclublem  14918  cotrtrclfv  14935  dfiso2  17696  efgcpbllemb  19684  frgpuplem  19701  lspsn  20953  mpfind  22070  pf1ind  22299  eltg  22901  eltg2  22902  islocfin  23461  fbssfi  23781  nosupres  27675  nosupbnd1lem3  27678  nosupbnd1lem5  27680  noinffv  27689  noinfres  27690  noinfbnd1lem3  27693  noinfbnd1lem5  27695  isewlk  29676  elabreximd  32585  abfmpunirn  32730  ellpi  33454  fmlafvel  35579  isfmlasuc  35582  r1peuqusdeg1  35837  poimirlem3  37824  poimirlem25  37846  islshpkrN  39380  sticksstones8  42407  sticksstones9  42408  sticksstones11  42410  sticksstones17  42417  sticksstones18  42418  rhmqusspan  42439  sn-iotalem  42477  setindtrs  43267  frege55lem1c  44157  nzss  44558  afvelrnb  47409  afvelrnb0  47410  dfatco  47502  elsetpreimafvb  47630  isgrim  48128  isgrlim  48228  discsntermlem  49815  basrestermcfolem  49816  setis  49943