Theorem moeq 3653

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2539  df-cleq 2728

This theorem is referenced by:  eueq  3654  mosub  3659  euxfr2w  3666  euxfr2  3668  reueq  3683  rmoeq  3684  reuxfrd  3694  sndisj  5077  disjxsn  5079  funopabeq  6534  funcnvsn  6548  fvmptg  6945  fvopab6  6982  mpofun  7491  ovmpt4g  7514  ov3  7530  ov6g  7531  abrexexg  7914  oprabex3  7930  1stconst  8050  2ndconst  8051  iunmapdisj  9945  axaddf  11068  axmulf  11069  joinfval  18337  joinval  18341  meetfval  18351  meetval  18355  reuxfrdf  32560  abrexdom2jm  32578  abrexdom2  38052  tfsconcatlem  43764  sinnpoly  47339