# Metamath Proof Explorer

## Theorem ax6vsep

Description: Derive ax6v (a weakened version of ax-6 where x and y must be distinct), from Separation ax-sep and Extensionality ax-ext . See ax6 for the derivation of ax-6 from ax6v . (Contributed by NM, 12-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6vsep ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$

### Proof

Step Hyp Ref Expression
1 ax-sep ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)\right)$
2 id ${⊢}{z}={z}\to {z}={z}$
3 2 biantru ${⊢}{z}\in {y}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)$
4 3 bibi2i ${⊢}\left({z}\in {x}↔{z}\in {y}\right)↔\left({z}\in {x}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)\right)$
5 4 biimpri ${⊢}\left({z}\in {x}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)\right)\to \left({z}\in {x}↔{z}\in {y}\right)$
6 5 alimi ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔{z}\in {y}\right)$
7 ax-ext ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔{z}\in {y}\right)\to {x}={y}$
8 6 7 syl ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)\right)\to {x}={y}$
9 8 eximi ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}\in {x}↔\left({z}\in {y}\wedge \left({z}={z}\to {z}={z}\right)\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
10 1 9 ax-mp ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
11 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
12 10 11 mpbi ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$