Theorem moeq 3648

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-cleq 2731

This theorem is referenced by:  eueq  3649  mosub  3654  euxfr2w  3661  euxfr2  3663  reueq  3678  rmoeq  3679  reuxfrd  3689  sndisj  5064  disjxsn  5066  funopabeq  6521  funcnvsn  6535  fvmptg  6933  fvopab6  6970  mpofun  7480  ovmpt4g  7503  ov3  7519  ov6g  7520  abrexexg  7903  oprabex3  7919  1stconst  8039  2ndconst  8040  iunmapdisj  9936  axaddf  11059  axmulf  11060  joinfval  18328  joinval  18332  meetfval  18342  meetval  18346  reuxfrdf  32578  abrexdom2jm  32596  abrexdom2  38098  tfsconcatlem  43781  sinnpoly  47354