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

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

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 2733

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

This theorem is used by:  eueq  3666  mosub  3671  euxfr2w  3678  euxfr2  3680  reueq  3695  rmoeq  3696  reuxfrd  3706  sndisj  5095  disjxsn  5097  funopabeq  6576  funcnvsn  6590  fvmptg  6991  fvopab6  7028  mpofun  7544  ovmpt4g  7567  ov3  7583  ov6g  7584  funmpt3  7687  mpt3fvd  7688  abrexexg  7973  oprabex3  7989  1stconst  8111  2ndconst  8112  iunmapdisj  10102  axaddf  11230  axmulf  11231  joinfval  18545  joinval  18549  meetfval  18559  meetval  18563  reuxfrdf  33087  abrexdom2jm  33104  abrexdom2  38665  tfsconcatlem  44337  sinnpoly  47940