Theorem elabg 3643

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 2370. (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 3638	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥(𝑥 = 𝐴 → (𝜑 ↔ 𝜓))) → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))
4	2, 3	mpan2 691	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ 𝜓))

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803

This theorem is referenced by:  elab  3646  elab2g  3647  elabd  3648  elab3g  3652  sbcieg  3793  intmin3  4940  elabrexg  7217  finds  7872  elfi  9364  inficl  9376  dffi3  9382  scott0  9839  elgch  10575  nqpr  10967  hashf1lem1  14420  cshword  14756  trclublem  14961  cotrtrclfv  14978  dfiso2  17734  efgcpbllemb  19685  frgpuplem  19702  lspsn  20908  mpfind  22014  pf1ind  22242  eltg  22844  eltg2  22845  islocfin  23404  fbssfi  23724  nosupres  27619  nosupbnd1lem3  27622  nosupbnd1lem5  27624  noinffv  27633  noinfres  27634  noinfbnd1lem3  27637  noinfbnd1lem5  27639  isewlk  29530  elabreximd  32439  abfmpunirn  32576  ellpi  33344  fmlafvel  35372  isfmlasuc  35375  r1peuqusdeg1  35630  poimirlem3  37617  poimirlem25  37639  islshpkrN  39113  sticksstones8  42141  sticksstones9  42142  sticksstones11  42144  sticksstones17  42151  sticksstones18  42152  rhmqusspan  42173  sn-iotalem  42209  setindtrs  43014  frege55lem1c  43905  nzss  44306  afvelrnb  47164  afvelrnb0  47165  dfatco  47257  elsetpreimafvb  47385  isgrim  47882  isgrlim  47981  discsntermlem  49559  basrestermcfolem  49560  setis  49687