Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axc9lem1 Structured version   Visualization version   Unicode version

Theorem axc9lem1 2106
 Description: A version of ax13v 2105 with one distinct variable restriction dropped. For convenience, is kept on the right side of equations. The proof of ax13 2155 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
Assertion
Ref Expression
axc9lem1
Distinct variable group:   ,

Proof of Theorem axc9lem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 equviniv 1880 . 2
2 ax13v 2105 . . . . 5
3 equequ2 1876 . . . . . . 7
43biimprcd 233 . . . . . 6
54alimdv 1771 . . . . 5
62, 5syl9 72 . . . 4
76impd 438 . . 3
87exlimdv 1787 . 2
91, 8syl5 32 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wa 376  wal 1450  wex 1671 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-13 2104 This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672 This theorem is referenced by:  ax6e  2107  axc9lem2  2146  axc9lem2OLD  2147  nfeqf2  2148
 Copyright terms: Public domain W3C validator