Theorem moeq 3665

Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3665 and eueq 3666. (Proof shortened by BJ, 24-Sep-2022.)

Assertion

Ref	Expression
moeq	⊢ ∃*𝑥 𝑥 = 𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem moeq

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqtr3 2758	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
2	1	gen2 1797	. 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
3		eqeq1 2740	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
4	3	mo4 2566	. 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦))
5	2, 4	mpbir 231	1 ⊢ ∃*𝑥 𝑥 = 𝐴

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃*wmo 2537

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-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-cleq 2728

This theorem is referenced by:  eueq  3666  mosub  3671  euxfr2w  3678  euxfr2  3680  reueq  3695  rmoeq  3696  reuxfrd  3706  sndisj  5090  disjxsn  5092  funopabeq  6528  funcnvsn  6542  fvmptg  6939  fvopab6  6975  mpofun  7482  ovmpt4g  7505  ov3  7521  ov6g  7522  abrexexg  7905  oprabex3  7921  1stconst  8042  2ndconst  8043  iunmapdisj  9933  axaddf  11056  axmulf  11057  joinfval  18294  joinval  18298  meetfval  18308  meetval  18312  reuxfrdf  32565  abrexdom2jm  32583  abrexdom2  37932  tfsconcatlem  43578  sinnpoly  47137