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

Theorem moeq 3699
Description: There exists at most one set equal to a given class. (Contributed by NM, 8-Mar-1995.) Shorten combined proofs of moeq 3699 and eueq 3700. (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 2751 . . 3 ((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
21gen2 1790 . 2 𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦)
3 eqeq1 2729 . . 3 (𝑥 = 𝑦 → (𝑥 = 𝐴𝑦 = 𝐴))
43mo4 2554 . 2 (∃*𝑥 𝑥 = 𝐴 ↔ ∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐴) → 𝑥 = 𝑦))
52, 4mpbir 230 1 ∃*𝑥 𝑥 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wal 1531   = wceq 1533  ∃*wmo 2526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-mo 2528  df-cleq 2717
This theorem is referenced by:  eueq  3700  mosub  3705  euxfr2w  3712  euxfr2  3714  reueq  3729  rmoeq  3730  reuxfrd  3740  sndisj  5140  disjxsn  5142  funopabeq  6590  funcnvsn  6604  fvmptg  7002  fvopab6  7038  mpofun  7544  ovmpt4g  7568  ov3  7584  ov6g  7585  abrexexg  7965  oprabex3  7982  1stconst  8105  2ndconst  8106  iunmapdisj  10048  axaddf  11170  axmulf  11171  joinfval  18368  joinval  18372  meetfval  18382  meetval  18386  reuxfrdf  32367  abrexdom2jm  32381  abrexdom2  37335  tfsconcatlem  42907
  Copyright terms: Public domain W3C validator