Theorem moeq 3678

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃*wmo 2531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-cleq 2721

This theorem is referenced by:  eueq  3679  mosub  3684  euxfr2w  3691  euxfr2  3693  reueq  3708  rmoeq  3709  reuxfrd  3719  sndisj  5099  disjxsn  5101  funopabeq  6552  funcnvsn  6566  fvmptg  6966  fvopab6  7002  mpofun  7513  ovmpt4g  7536  ov3  7552  ov6g  7553  abrexexg  7939  oprabex3  7956  1stconst  8079  2ndconst  8080  iunmapdisj  9976  axaddf  11098  axmulf  11099  joinfval  18332  joinval  18336  meetfval  18346  meetval  18350  reuxfrdf  32420  abrexdom2jm  32437  abrexdom2  37725  tfsconcatlem  43325  sinnpoly  46892