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

Theorem cleljustALT 2384
Description: Alternate proof of cleljust 2124. 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 disjoint variable 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 1912 . . 3 (𝑥𝑦 → ∀𝑧 𝑥𝑦)
2 elequ1 2122 . . 3 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
31, 2equsexhv 2302 . 2 (∃𝑧(𝑧 = 𝑥𝑧𝑦) ↔ 𝑥𝑦)
43bicomi 227 1 (𝑥𝑦 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-10 2146  ax-12 2179
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator