New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax10-16 Unicode 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
Distinct variable group:   ,

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