Theorem moeq 3697

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

Syntax hints:   → wi 4   ∧ wa 398  ∀wal 1531   = wceq 1533  ∃*wmo 2616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-mo 2618  df-cleq 2814

This theorem is referenced by:  eueq  3698  mosub  3703  euxfr2w  3710  euxfr2  3712  reueq  3727  rmoeq  3728  reuxfrd  3738  sndisj  5049  disjxsn  5051  funopabeq  6385  funcnvsn  6398  fvmptg  6760  fvopab6  6795  ovmpt4g  7291  ov3  7305  ov6g  7306  oprabex3  7672  1stconst  7789  2ndconst  7790  iunmapdisj  9443  axaddf  10561  axmulf  10562  joinfval  17605  joinval  17609  meetfval  17619  meetval  17623  reuxfrdf  30249  abrexdom2jm  30262  abrexdom2  35000