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.) (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-1 5  ax-2 6  ax-3 7  ax-mp 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