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 2782	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
2	1	gen2 1829	. 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
3		eqeq1 2764	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
4	3	mo4 2591	. 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦))
5	2, 4	mpbir 234	1 ⊢ ∃*𝑥 𝑥 = 𝐴

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃*wmo 2562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2564  df-cleq 2752

This theorem is used by:  eueq  3666  mosub  3671  euxfr2w  3678  euxfr2  3680  reueq  3695  rmoeq  3696  reuxfrd  3706  sndisj  5095  disjxsn  5097  funopabeq  6570  funcnvsn  6584  fvmptg  6985  fvopab6  7022  mpofun  7538  ovmpt4g  7561  ov3  7577  ov6g  7578  abrexexg  7959  oprabex3  7975  1stconst  8098  2ndconst  8099  iunmapdisj  10027  axaddf  11155  axmulf  11156  joinfval  18460  joinval  18464  meetfval  18474  meetval  18478  reuxfrdf  32967  abrexdom2jm  32984  abrexdom2  38482  tfsconcatlem  44178  sinnpoly  47760