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

Theorem cleljustALT 2347
Description: Alternate proof of cleljust 2153. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how DV conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
cleljustALT (𝑥𝑦 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝑦))
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧

Proof of Theorem cleljustALT
StepHypRef Expression
1 ax-5 1991 . . 3 (𝑥𝑦 → ∀𝑧 𝑥𝑦)
2 elequ1 2152 . . 3 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
31, 2equsexhv 2288 . 2 (∃𝑧(𝑧 = 𝑥𝑧𝑦) ↔ 𝑥𝑦)
43bicomi 214 1 (𝑥𝑦 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-10 2174  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-nf 1858
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator