Theorem moeq 3613

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

Syntax hints:   → wi 4   ∧ wa 387  ∀wal 1505   = wceq 1507  ∃*wmo 2545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2751

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-cleq 2772

This theorem is referenced by:  eueq  3614  mosub  3619  euxfr2  3626  reueq  3641  rmoeq  3642  reuxfr3d  3652  sndisj  4921  disjxsn  4923  funopabeq  6224  funcnvsn  6237  fvmptg  6593  fvopab6  6626  ovmpt4g  7113  ov3  7127  ov6g  7128  oprabex3  7490  1stconst  7603  2ndconst  7604  iunmapdisj  9243  axaddf  10365  axmulf  10366  joinfval  17469  joinval  17473  meetfval  17483  meetval  17487  abrexdom2jm  30047  abrexdom2  34445