Theorem moeq 3667

Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3667 and eueq 3668. (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  3668  mosub  3673  euxfr2w  3680  euxfr2  3682  reueq  3697  rmoeq  3698  reuxfrd  3708  sndisj  5084  disjxsn  5086  funopabeq  6518  funcnvsn  6532  fvmptg  6928  fvopab6  6964  mpofun  7473  ovmpt4g  7496  ov3  7512  ov6g  7513  abrexexg  7896  oprabex3  7912  1stconst  8033  2ndconst  8034  iunmapdisj  9917  axaddf  11039  axmulf  11040  joinfval  18277  joinval  18281  meetfval  18291  meetval  18295  reuxfrdf  32435  abrexdom2jm  32452  abrexdom2  37715  tfsconcatlem  43313  sinnpoly  46879