Theorem moeq 3637

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-mo 2540  df-cleq 2730

This theorem is referenced by:  eueq  3638  mosub  3643  euxfr2w  3650  euxfr2  3652  reueq  3667  rmoeq  3668  reuxfrd  3678  sndisj  5061  disjxsn  5063  funopabeq  6454  funcnvsn  6468  fvmptg  6855  fvopab6  6890  mpofun  7376  ovmpt4g  7398  ov3  7413  ov6g  7414  oprabex3  7793  1stconst  7911  2ndconst  7912  iunmapdisj  9710  axaddf  10832  axmulf  10833  joinfval  18006  joinval  18010  meetfval  18020  meetval  18024  reuxfrdf  30740  abrexdom2jm  30754  abrexdom2  35816