Theorem moeq 3690

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eueq  3691  mosub  3696  euxfr2w  3703  euxfr2  3705  reueq  3720  rmoeq  3721  reuxfrd  3731  sndisj  5111  disjxsn  5113  funopabeq  6572  funcnvsn  6586  fvmptg  6984  fvopab6  7020  mpofun  7531  ovmpt4g  7554  ov3  7570  ov6g  7571  abrexexg  7959  oprabex3  7976  1stconst  8099  2ndconst  8100  iunmapdisj  10037  axaddf  11159  axmulf  11160  joinfval  18383  joinval  18387  meetfval  18397  meetval  18401  reuxfrdf  32472  abrexdom2jm  32489  abrexdom2  37755  tfsconcatlem  43360