Theorem moeq 3661

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃*wmo 2533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2535  df-cleq 2723

This theorem is referenced by:  eueq  3662  mosub  3667  euxfr2w  3674  euxfr2  3676  reueq  3691  rmoeq  3692  reuxfrd  3702  sndisj  5081  disjxsn  5083  funopabeq  6517  funcnvsn  6531  fvmptg  6927  fvopab6  6963  mpofun  7470  ovmpt4g  7493  ov3  7509  ov6g  7510  abrexexg  7893  oprabex3  7909  1stconst  8030  2ndconst  8031  iunmapdisj  9914  axaddf  11036  axmulf  11037  joinfval  18277  joinval  18281  meetfval  18291  meetval  18295  reuxfrdf  32470  abrexdom2jm  32488  abrexdom2  37781  tfsconcatlem  43439  sinnpoly  47001