Theorem moeq 3675

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

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃*wmo 2531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-cleq 2721

This theorem is referenced by:  eueq  3676  mosub  3681  euxfr2w  3688  euxfr2  3690  reueq  3705  rmoeq  3706  reuxfrd  3716  sndisj  5094  disjxsn  5096  funopabeq  6536  funcnvsn  6550  fvmptg  6948  fvopab6  6984  mpofun  7493  ovmpt4g  7516  ov3  7532  ov6g  7533  abrexexg  7919  oprabex3  7935  1stconst  8056  2ndconst  8057  iunmapdisj  9952  axaddf  11074  axmulf  11075  joinfval  18308  joinval  18312  meetfval  18322  meetval  18326  reuxfrdf  32393  abrexdom2jm  32410  abrexdom2  37698  tfsconcatlem  43298  sinnpoly  46865