Theorem moeq 3713

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eueq  3714  mosub  3719  euxfr2w  3726  euxfr2  3728  reueq  3743  rmoeq  3744  reuxfrd  3754  sndisj  5135  disjxsn  5137  funopabeq  6602  funcnvsn  6616  fvmptg  7014  fvopab6  7050  mpofun  7557  ovmpt4g  7580  ov3  7596  ov6g  7597  abrexexg  7985  oprabex3  8002  1stconst  8125  2ndconst  8126  iunmapdisj  10063  axaddf  11185  axmulf  11186  joinfval  18418  joinval  18422  meetfval  18432  meetval  18436  reuxfrdf  32510  abrexdom2jm  32527  abrexdom2  37738  tfsconcatlem  43349