Theorem moeq 3648

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-mo 2543  df-cleq 2731

This theorem is referenced by:  eueq  3649  mosub  3654  euxfr2w  3661  euxfr2  3663  reueq  3678  rmoeq  3679  reuxfrd  3689  sndisj  5065  disjxsn  5067  funopabeq  6522  funcnvsn  6536  fvmptg  6934  fvopab6  6971  mpofun  7481  ovmpt4g  7504  ov3  7520  ov6g  7521  abrexexg  7904  oprabex3  7920  1stconst  8040  2ndconst  8041  iunmapdisj  9937  axaddf  11060  axmulf  11061  joinfval  18329  joinval  18333  meetfval  18343  meetval  18347  reuxfrdf  32579  abrexdom2jm  32597  abrexdom2  38107  tfsconcatlem  43790  sinnpoly  47362