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

Theorem axc9lem1 2001
Description: A version of ax13v 2000 with one distinct variable restriction dropped. For convenience, is kept on the right side of equations. The proof of ax13 2047 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 1803 . 2
2 ax13v 2000 . . . . 5
3 equequ2 1799 . . . . . . 7
43biimprcd 225 . . . . . 6
54alimdv 1709 . . . . 5
62, 5syl9 71 . . . 4
76impd 431 . . 3
87exlimdv 1724 . 2
91, 8syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  A.wal 1393  E.wex 1612
This theorem is referenced by:  ax6e  2002  axc9lem2  2040  nfeqf2  2041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613
  Copyright terms: Public domain W3C validator