Theorem moeq 3622

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

Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1537   = wceq 1539  ∃*wmo 2556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-mo 2558  df-cleq 2751

This theorem is referenced by:  eueq  3623  mosub  3628  euxfr2w  3635  euxfr2  3637  reueq  3652  rmoeq  3653  reuxfrd  3663  sndisj  5024  disjxsn  5026  funopabeq  6372  funcnvsn  6386  fvmptg  6758  fvopab6  6793  mpofun  7271  ovmpt4g  7293  ov3  7308  ov6g  7309  oprabex3  7683  1stconst  7801  2ndconst  7802  iunmapdisj  9484  axaddf  10606  axmulf  10607  joinfval  17678  joinval  17682  meetfval  17692  meetval  17696  reuxfrdf  30362  abrexdom2jm  30376  abrexdom2  35450