Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  moeq Structured version   Visualization version   GIF version

Theorem moeq 3622
 Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3622 and eueq 3623. (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.
StepHypRef Expression
1 eqtr3 2781 . . 3 ((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
21gen2 1799 . 2 𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
3 eqeq1 2763 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43mo4 2585 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦))
52, 4mpbir 234 1 ∃*𝑥 𝑥 = 𝐴
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400  ∀wal 1537   = wceq 1539  ∃*wmo 2556 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 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-mo 2558  df-cleq 2751 This theorem is referenced by:  eueq  3623  mosub  3628  euxfr2w  3635  euxfr2  3637  reueq  3652  rmoeq  3653  reuxfrd  3663  sndisj  5024  disjxsn  5026  funopabeq  6372  funcnvsn  6386  fvmptg  6758  fvopab6  6793  mpofun  7271  ovmpt4g  7293  ov3  7308  ov6g  7309  oprabex3  7683  1stconst  7801  2ndconst  7802  iunmapdisj  9484  axaddf  10606  axmulf  10607  joinfval  17678  joinval  17682  meetfval  17692  meetval  17696  reuxfrdf  30362  abrexdom2jm  30376  abrexdom2  35450
 Copyright terms: Public domain W3C validator