Theorem moeq 3654

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-cleq 2729

This theorem is referenced by:  eueq  3655  mosub  3660  euxfr2w  3667  euxfr2  3669  reueq  3684  rmoeq  3685  reuxfrd  3695  sndisj  5078  disjxsn  5080  funopabeq  6529  funcnvsn  6543  fvmptg  6940  fvopab6  6977  mpofun  7485  ovmpt4g  7508  ov3  7524  ov6g  7525  abrexexg  7908  oprabex3  7924  1stconst  8044  2ndconst  8045  iunmapdisj  9939  axaddf  11062  axmulf  11063  joinfval  18331  joinval  18335  meetfval  18345  meetval  18349  reuxfrdf  32578  abrexdom2jm  32596  abrexdom2  38069  tfsconcatlem  43785  sinnpoly  47354