New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  cleljust GIF version

Theorem cleljust 2014
 Description: When the class variables in definition df-clel 2349 are replaced with setvar variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the setvar variables in wel 1711 with the class variables in wcel 1710. Note: This proof is referenced on the Metamath Proof Explorer Home Page and shouldn't be changed. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.)
Assertion
Ref Expression
cleljust (x yz(z = x z y))
Distinct variable groups:   x,z   y,z

Proof of Theorem cleljust
StepHypRef Expression
1 ax-17 1616 . . 3 (x yz x y)
2 elequ1 1713 . . 3 (z = x → (z yx y))
31, 2equsexh 1963 . 2 (z(z = x z y) ↔ x y)
43bicomi 193 1 (x yz(z = x z y))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator