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

Theorem ax10-16 2190
 Description: This theorem shows that, given ax-16 2144, we can derive a version of ax-10 2140. However, it is weaker than ax-10 2140 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 27-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ax10-16 (x x = zz z = x)
Distinct variable group:   x,z

Proof of Theorem ax10-16
Dummy variable w is distinct from all other variables.
StepHypRef Expression
1 ax-16 2144 . . . 4 (x x = z → (x = wx x = w))
21alrimiv 1631 . . 3 (x x = zw(x = wx x = w))
32a5i-o 2150 . 2 (x x = zxw(x = wx x = w))
4 equequ1 1684 . . . . . 6 (x = z → (x = wz = w))
54cbvalv 2002 . . . . . . 7 (x x = wz z = w)
65a1i 10 . . . . . 6 (x = z → (x x = wz z = w))
74, 6imbi12d 311 . . . . 5 (x = z → ((x = wx x = w) ↔ (z = wz z = w)))
87albidv 1625 . . . 4 (x = z → (w(x = wx x = w) ↔ w(z = wz z = w)))
98cbvalv 2002 . . 3 (xw(x = wx x = w) ↔ zw(z = wz z = w))
109biimpi 186 . 2 (xw(x = wx x = w) → zw(z = wz z = w))
11 nfa1-o 2166 . . . . . . 7 zz z = w
121119.23 1801 . . . . . 6 (z(z = wz z = w) ↔ (z z = wz z = w))
1312albii 1566 . . . . 5 (wz(z = wz z = w) ↔ w(z z = wz z = w))
14 a9ev 1656 . . . . . . . 8 z z = w
15 pm2.27 35 . . . . . . . 8 (z z = w → ((z z = wz z = w) → z z = w))
1614, 15ax-mp 8 . . . . . . 7 ((z z = wz z = w) → z z = w)
1716alimi 1559 . . . . . 6 (w(z z = wz z = w) → wz z = w)
18 equequ2 1686 . . . . . . . . 9 (w = x → (z = wz = x))
1918spv 1998 . . . . . . . 8 (w z = wz = x)
2019sps-o 2159 . . . . . . 7 (zw z = wz = x)
2120a7s 1735 . . . . . 6 (wz z = wz = x)
2217, 21syl 15 . . . . 5 (w(z z = wz z = w) → z = x)
2313, 22sylbi 187 . . . 4 (wz(z = wz z = w) → z = x)
2423a7s 1735 . . 3 (zw(z = wz z = w) → z = x)
2524a5i-o 2150 . 2 (zw(z = wz z = w) → z z = x)
263, 10, 253syl 18 1 (x x = zz z = x)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176  ∀wal 1540  ∃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-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-4 2135  ax-5o 2136  ax-6o 2137  ax-16 2144 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