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

Theorem moeq 3535
Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3535 and eueq 3536. (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 2786 . . 3 ((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
21gen2 1891 . 2 𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
3 eqeq1 2769 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43mo4 2638 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦))
52, 4mpbir 222 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1650   = wceq 1652  ∃*wmo 2563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2565  df-cleq 2758
This theorem is referenced by:  eueq  3536  mosub  3543  euxfr2  3550  reueq  3565  rmoeq  3566  sndisj  4801  disjxsn  4803  reuxfr2d  5054  funopabeq  6104  funcnvsn  6117  fvmptg  6469  fvopab6  6500  ovmpt4g  6981  ov3  6995  ov6g  6996  oprabex3  7355  1stconst  7467  2ndconst  7468  iunmapdisj  9097  axaddf  10219  axmulf  10220  joinfval  17269  joinval  17273  meetfval  17283  meetval  17287  reuxfr3d  29718  abrexdom2jm  29730  abrexdom2  33881
  Copyright terms: Public domain W3C validator