Theorem moeq 3664

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃*wmo 2562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564  df-cleq 2752

This theorem is used by:  eueq  3665  mosub  3670  euxfr2w  3677  euxfr2  3679  reueq  3694  rmoeq  3695  reuxfrd  3705  sndisj  5094  disjxsn  5096  funopabeq  6581  funcnvsn  6595  fvmptg  6996  fvopab6  7033  mpofun  7548  ovmpt4g  7571  ov3  7587  ov6g  7588  funmpt3  7691  mpt3fvd  7692  abrexexg  7977  oprabex3  7993  1stconst  8118  2ndconst  8119  iunmapdisj  10109  axaddf  11237  axmulf  11238  joinfval  18554  joinval  18558  meetfval  18568  meetval  18572  reuxfrdf  33138  abrexdom2jm  33155  abrexdom2  38802  tfsconcatlem  44475  sinnpoly  48077