Theorem moeq 3663

Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3663 and eueq 3664. (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 2756	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
2	1	gen2 1797	. 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
3		eqeq1 2738	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
4	3	mo4 2564	. 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦))
5	2, 4	mpbir 231	1 ⊢ ∃*𝑥 𝑥 = 𝐴

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

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 2706

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

This theorem is referenced by:  eueq  3664  mosub  3669  euxfr2w  3676  euxfr2  3678  reueq  3693  rmoeq  3694  reuxfrd  3704  sndisj  5088  disjxsn  5090  funopabeq  6526  funcnvsn  6540  fvmptg  6937  fvopab6  6973  mpofun  7480  ovmpt4g  7503  ov3  7519  ov6g  7520  abrexexg  7903  oprabex3  7919  1stconst  8040  2ndconst  8041  iunmapdisj  9931  axaddf  11054  axmulf  11055  joinfval  18292  joinval  18296  meetfval  18306  meetval  18310  reuxfrdf  32514  abrexdom2jm  32532  abrexdom2  37871  tfsconcatlem  43520  sinnpoly  47079