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 2759	. . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
2	1	gen2 1798	. 2 ⊢ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦)
3		eqeq1 2741	. . 3 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝐴 ↔ 𝑦 = 𝐴))
4	3	mo4 2567	. 2 ⊢ (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥∀𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐴) → 𝑥 = 𝑦))
5	2, 4	mpbir 231	1 ⊢ ∃*𝑥 𝑥 = 𝐴

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

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 2709

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

This theorem is referenced by:  eueq  3668  mosub  3673  euxfr2w  3680  euxfr2  3682  reueq  3697  rmoeq  3698  reuxfrd  3708  sndisj  5092  disjxsn  5094  funopabeq  6536  funcnvsn  6550  fvmptg  6947  fvopab6  6984  mpofun  7492  ovmpt4g  7515  ov3  7531  ov6g  7532  abrexexg  7915  oprabex3  7931  1stconst  8052  2ndconst  8053  iunmapdisj  9945  axaddf  11068  axmulf  11069  joinfval  18306  joinval  18310  meetfval  18320  meetval  18324  reuxfrdf  32577  abrexdom2jm  32595  abrexdom2  37982  tfsconcatlem  43693  sinnpoly  47251