Theorem moeq 3699

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

Syntax hints:   → wi 4   ∧ wa 394  ∀wal 1531   = wceq 1533  ∃*wmo 2526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-mo 2528  df-cleq 2717

This theorem is referenced by:  eueq  3700  mosub  3705  euxfr2w  3712  euxfr2  3714  reueq  3729  rmoeq  3730  reuxfrd  3740  sndisj  5140  disjxsn  5142  funopabeq  6590  funcnvsn  6604  fvmptg  7002  fvopab6  7038  mpofun  7544  ovmpt4g  7568  ov3  7584  ov6g  7585  abrexexg  7965  oprabex3  7982  1stconst  8105  2ndconst  8106  iunmapdisj  10048  axaddf  11170  axmulf  11171  joinfval  18368  joinval  18372  meetfval  18382  meetval  18386  reuxfrdf  32367  abrexdom2jm  32381  abrexdom2  37335  tfsconcatlem  42907