Theorem moeq 3679

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

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1565   = wceq 1567  ∃*wmo 2571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573  df-cleq 2761

This theorem is referenced by:  eueq  3680  mosub  3685  euxfr2w  3692  euxfr2  3694  reueq  3709  rmoeq  3710  reuxfrd  3720  sndisj  5105  disjxsn  5107  funopabeq  6573  funcnvsn  6587  fvmptg  6988  fvopab6  7025  mpofun  7535  ovmpt4g  7558  ov3  7574  ov6g  7575  abrexexg  7957  oprabex3  7973  1stconst  8094  2ndconst  8095  iunmapdisj  10006  axaddf  11129  axmulf  11130  joinfval  18426  joinval  18430  meetfval  18440  meetval  18444  reuxfrdf  32777  abrexdom2jm  32794  abrexdom2  38269  tfsconcatlem  43954  sinnpoly  47516