Theorem moeq 3670

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

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1558   = wceq 1560  ∃*wmo 2564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-mo 2566  df-cleq 2754

This theorem is referenced by:  eueq  3671  mosub  3676  euxfr2w  3683  euxfr2  3685  reueq  3700  rmoeq  3701  reuxfrd  3711  sndisj  5092  disjxsn  5094  funopabeq  6557  funcnvsn  6571  fvmptg  6973  fvopab6  7010  mpofun  7520  ovmpt4g  7543  ov3  7559  ov6g  7560  abrexexg  7942  oprabex3  7958  1stconst  8079  2ndconst  8080  iunmapdisj  9979  axaddf  11103  axmulf  11104  joinfval  18403  joinval  18407  meetfval  18417  meetval  18421  reuxfrdf  32690  abrexdom2jm  32707  abrexdom2  38230  tfsconcatlem  43913  sinnpoly  47485