Theorem moeq 3729

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃*wmo 2541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-cleq 2732

This theorem is referenced by:  eueq  3730  mosub  3735  euxfr2w  3742  euxfr2  3744  reueq  3759  rmoeq  3760  reuxfrd  3770  sndisj  5158  disjxsn  5160  funopabeq  6614  funcnvsn  6628  fvmptg  7027  fvopab6  7063  mpofun  7574  ovmpt4g  7597  ov3  7613  ov6g  7614  abrexexg  8001  oprabex3  8018  1stconst  8141  2ndconst  8142  iunmapdisj  10092  axaddf  11214  axmulf  11215  joinfval  18443  joinval  18447  meetfval  18457  meetval  18461  reuxfrdf  32519  abrexdom2jm  32536  abrexdom2  37691  tfsconcatlem  43298