Theorem moeq 3716

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃*wmo 2536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-mo 2538  df-cleq 2727

This theorem is referenced by:  eueq  3717  mosub  3722  euxfr2w  3729  euxfr2  3731  reueq  3746  rmoeq  3747  reuxfrd  3757  sndisj  5140  disjxsn  5142  funopabeq  6604  funcnvsn  6618  fvmptg  7014  fvopab6  7050  mpofun  7557  ovmpt4g  7580  ov3  7596  ov6g  7597  abrexexg  7984  oprabex3  8001  1stconst  8124  2ndconst  8125  iunmapdisj  10061  axaddf  11183  axmulf  11184  joinfval  18431  joinval  18435  meetfval  18445  meetval  18449  reuxfrdf  32519  abrexdom2jm  32536  abrexdom2  37718  tfsconcatlem  43326