Theorem moeq 3668

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eueq  3669  mosub  3674  euxfr2w  3681  euxfr2  3683  reueq  3698  rmoeq  3699  reuxfrd  3709  sndisj  5100  disjxsn  5102  funopabeq  6604  funcnvsn  6620  fvmptg  7022  fvopab6  7059  mpofun  7575  ovmpt4g  7599  ov3  7615  ov6g  7616  funmpt3  7719  mpt3fvd  7720  abrexexg  8007  oprabex3  8023  1stconst  8148  2ndconst  8149  iunmapdisj  10141  axaddf  11269  axmulf  11270  joinfval  18595  joinval  18599  meetfval  18609  meetval  18613  reuxfrdf  33186  abrexdom2jm  33203  mpofvd  35838  abrexdom2  38933  tfsconcatlem  44599  sinnpoly  48214