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

Theorem moeq 3713
Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3713 and eueq 3714. (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 2763 . . 3 ((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
21gen2 1796 . 2 𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
3 eqeq1 2741 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43mo4 2566 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦))
52, 4mpbir 231 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wal 1538   = wceq 1540  ∃*wmo 2538
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 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-cleq 2729
This theorem is referenced by:  eueq  3714  mosub  3719  euxfr2w  3726  euxfr2  3728  reueq  3743  rmoeq  3744  reuxfrd  3754  sndisj  5135  disjxsn  5137  funopabeq  6602  funcnvsn  6616  fvmptg  7014  fvopab6  7050  mpofun  7557  ovmpt4g  7580  ov3  7596  ov6g  7597  abrexexg  7985  oprabex3  8002  1stconst  8125  2ndconst  8126  iunmapdisj  10063  axaddf  11185  axmulf  11186  joinfval  18418  joinval  18422  meetfval  18432  meetval  18436  reuxfrdf  32510  abrexdom2jm  32527  abrexdom2  37738  tfsconcatlem  43349
  Copyright terms: Public domain W3C validator