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

Theorem cleljustALT 2173
Description: Alternate proof of cleljust 1985. 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 1827 . . 3 (𝑥𝑦 → ∀𝑧 𝑥𝑦)
2 elequ1 1984 . . 3 (𝑧 = 𝑥 → (𝑧𝑦𝑥𝑦))
31, 2equsexhv 2135 . 2 (∃𝑧(𝑧 = 𝑥𝑧𝑦) ↔ 𝑥𝑦)
43bicomi 213 1 (𝑥𝑦 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-10 2006  ax-12 2034
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-nf 1701
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator