Theorem moeq 3672

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  eueq  3673  mosub  3678  euxfr2w  3685  euxfr2  3687  reueq  3702  rmoeq  3703  reuxfrd  3713  sndisj  5103  disjxsn  5105  funopabeq  6576  funcnvsn  6590  fvmptg  6991  fvopab6  7028  mpofun  7543  ovmpt4g  7566  ov3  7582  ov6g  7583  abrexexg  7964  oprabex3  7980  1stconst  8101  2ndconst  8102  iunmapdisj  10023  axaddf  11147  axmulf  11148  joinfval  18451  joinval  18455  meetfval  18465  meetval  18469  reuxfrdf  32910  abrexdom2jm  32927  abrexdom2  38442  tfsconcatlem  44123  sinnpoly  47688