Theorem elabg 3628

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

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808

This theorem is referenced by:  elab  3631  elab2g  3632  elabd  3633  elab3g  3637  sbcieg  3777  intmin3  4928  elabrexg  7185  finds  7834  elfi  9306  inficl  9318  dffi3  9324  scott0  9788  elgch  10522  nqpr  10914  hashf1lem1  14366  cshword  14702  trclublem  14906  cotrtrclfv  14923  dfiso2  17683  efgcpbllemb  19671  frgpuplem  19688  lspsn  20939  mpfind  22045  pf1ind  22273  eltg  22875  eltg2  22876  islocfin  23435  fbssfi  23755  nosupres  27649  nosupbnd1lem3  27652  nosupbnd1lem5  27654  noinffv  27663  noinfres  27664  noinfbnd1lem3  27667  noinfbnd1lem5  27669  isewlk  29585  elabreximd  32494  abfmpunirn  32638  ellpi  33347  fmlafvel  35452  isfmlasuc  35455  r1peuqusdeg1  35710  poimirlem3  37686  poimirlem25  37708  islshpkrN  39242  sticksstones8  42269  sticksstones9  42270  sticksstones11  42272  sticksstones17  42279  sticksstones18  42280  rhmqusspan  42301  sn-iotalem  42342  setindtrs  43145  frege55lem1c  44036  nzss  44437  afvelrnb  47290  afvelrnb0  47291  dfatco  47383  elsetpreimafvb  47511  isgrim  48009  isgrlim  48109  discsntermlem  49698  basrestermcfolem  49699  setis  49826