**Description:** A commuted form of ax6ev . (Contributed by BJ, 7-Dec-2020)

Ref | Expression | ||
---|---|---|---|

Assertion | ax6evr | $${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{y}={x}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | ax6ev | $${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$$ | |

2 | equcomiv | $${\u22a2}{x}={y}\to {y}={x}$$ | |

3 | 1 2 | eximii | $${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{y}={x}$$ |