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

Theorem cleljustALT 2322
 Description: Alternate proof of cleljust 2139. 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 1980 . . 3 (𝑥𝑦 → ∀𝑧 𝑥𝑦)
2 elequ1 2138 . . 3 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
31, 2equsexhv 2263 . 2 (∃𝑧(𝑧 = 𝑥𝑧𝑦) ↔ 𝑥𝑦)
43bicomi 214 1 (𝑥𝑦 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝑦))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1845 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-10 2160  ax-12 2188 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1846  df-nf 1851 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator