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

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.
StepHypRef Expression
1 eqtr3 2802 . . 3 ((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
21gen2 1759 . 2 𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
3 eqeq1 2783 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43mo4 2582 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦))
52, 4mpbir 223 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator