Theorem moeq 3670

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

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-cleq 2755

This theorem is referenced by:  eueq  3671  mosub  3676  euxfr2w  3683  euxfr2  3685  reueq  3700  rmoeq  3701  reuxfrd  3711  sndisj  5101  disjxsn  5103  funopabeq  6572  funcnvsn  6586  fvmptg  6987  fvopab6  7024  mpofun  7534  ovmpt4g  7557  ov3  7573  ov6g  7574  abrexexg  7954  oprabex3  7970  1stconst  8091  2ndconst  8092  iunmapdisj  10003  axaddf  11125  axmulf  11126  joinfval  18422  joinval  18426  meetfval  18436  meetval  18440  reuxfrdf  32837  abrexdom2jm  32854  abrexdom2  38402  tfsconcatlem  44083  sinnpoly  47648