Theorem moeq 3643

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

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

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-mo 2541  df-cleq 2731

This theorem is referenced by:  eueq  3644  mosub  3649  euxfr2w  3656  euxfr2  3658  reueq  3673  rmoeq  3674  reuxfrd  3684  sndisj  5066  disjxsn  5068  funopabeq  6477  funcnvsn  6491  fvmptg  6882  fvopab6  6917  mpofun  7407  ovmpt4g  7429  ov3  7444  ov6g  7445  abrexexg  7812  oprabex3  7829  1stconst  7949  2ndconst  7950  iunmapdisj  9788  axaddf  10910  axmulf  10911  joinfval  18100  joinval  18104  meetfval  18114  meetval  18118  reuxfrdf  30848  abrexdom2jm  30862  abrexdom2  35898