Theorem moeq 3704

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535  df-cleq 2725

This theorem is referenced by:  eueq  3705  mosub  3710  euxfr2w  3717  euxfr2  3719  reueq  3734  rmoeq  3735  reuxfrd  3745  sndisj  5140  disjxsn  5142  funopabeq  6585  funcnvsn  6599  fvmptg  6997  fvopab6  7032  mpofun  7532  ovmpt4g  7555  ov3  7570  ov6g  7571  abrexexg  7947  oprabex3  7964  1stconst  8086  2ndconst  8087  iunmapdisj  10018  axaddf  11140  axmulf  11141  joinfval  18326  joinval  18330  meetfval  18340  meetval  18344  reuxfrdf  31731  abrexdom2jm  31745  abrexdom2  36599  tfsconcatlem  42086