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

Theorem cleljustALT 2015
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. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) (Revised by Mario Carneiro, 21-Dec-2016.)
Assertion
Ref Expression
cleljustALT (x yz(z = x z y))
Distinct variable groups:   x,z   y,z

Proof of Theorem cleljustALT
StepHypRef Expression
1 nfv 1619 . . 3 z x y
2 elequ1 1713 . . 3 (z = x → (z yx y))
31, 2equsex 1962 . 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