Theorem moeq 3681

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

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

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 2702

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

This theorem is referenced by:  eueq  3682  mosub  3687  euxfr2w  3694  euxfr2  3696  reueq  3711  rmoeq  3712  reuxfrd  3722  sndisj  5102  disjxsn  5104  funopabeq  6555  funcnvsn  6569  fvmptg  6969  fvopab6  7005  mpofun  7516  ovmpt4g  7539  ov3  7555  ov6g  7556  abrexexg  7942  oprabex3  7959  1stconst  8082  2ndconst  8083  iunmapdisj  9983  axaddf  11105  axmulf  11106  joinfval  18339  joinval  18343  meetfval  18353  meetval  18357  reuxfrdf  32427  abrexdom2jm  32444  abrexdom2  37732  tfsconcatlem  43332