ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax6evr Unicode version

Theorem ax6evr 1636
Description: A commuted form of a9ev 1630. The naming reflects how axioms were numbered in the Metamath Proof Explorer as of 2020 (a numbering which we eventually plan to adopt here too, but until this happens everywhere only some theorems will have it). (Contributed by BJ, 7-Dec-2020.)
Assertion
Ref Expression
ax6evr  |-  E. x  y  =  x
Distinct variable group:    x, y

Proof of Theorem ax6evr
StepHypRef Expression
1 a9ev 1630 . 2  |-  E. x  x  =  y
2 equcomi 1635 . 2  |-  ( x  =  y  ->  y  =  x )
31, 2eximii 1536 1  |-  E. x  y  =  x
Colors of variables: wff set class
Syntax hints:   E.wex 1424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470
This theorem depends on definitions:  df-bi 115
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator