# Metamath Proof Explorer

## Theorem ax6e2ndeq

Description: "At least two sets exist" expressed in the form of dtru is logically equivalent to the same expressed in a form similar to ax6e if dtru is false implies u = v . ax6e2ndeq is derived from ax6e2ndeqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2ndeq ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$

### Proof

Step Hyp Ref Expression
1 ax6e2nd ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$
2 ax6e2eq ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({u}={v}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\right)$
3 1 a1d ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left({u}={v}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\right)$
4 2 3 pm2.61i ${⊢}{u}={v}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$
5 1 4 jaoi ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$
6 olc ${⊢}{u}={v}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)$
7 6 a1d ${⊢}{u}={v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)\right)$
8 excom ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$
9 neeq1 ${⊢}{x}={u}\to \left({x}\ne {v}↔{u}\ne {v}\right)$
10 9 biimprcd ${⊢}{u}\ne {v}\to \left({x}={u}\to {x}\ne {v}\right)$
11 10 adantrd ${⊢}{u}\ne {v}\to \left(\left({x}={u}\wedge {y}={v}\right)\to {x}\ne {v}\right)$
12 simpr ${⊢}\left({x}={u}\wedge {y}={v}\right)\to {y}={v}$
13 12 a1i ${⊢}{u}\ne {v}\to \left(\left({x}={u}\wedge {y}={v}\right)\to {y}={v}\right)$
14 neeq2 ${⊢}{y}={v}\to \left({x}\ne {y}↔{x}\ne {v}\right)$
15 14 biimprcd ${⊢}{x}\ne {v}\to \left({y}={v}\to {x}\ne {y}\right)$
16 11 13 15 syl6c ${⊢}{u}\ne {v}\to \left(\left({x}={u}\wedge {y}={v}\right)\to {x}\ne {y}\right)$
17 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to {x}={y}$
18 17 necon3ai ${⊢}{x}\ne {y}\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
19 16 18 syl6 ${⊢}{u}\ne {v}\to \left(\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
20 19 eximdv ${⊢}{u}\ne {v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
21 nfnae ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
22 21 19.9 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
23 20 22 syl6ib ${⊢}{u}\ne {v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
24 23 eximdv ${⊢}{u}\ne {v}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
25 8 24 syl5bi ${⊢}{u}\ne {v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
26 nfnae ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
27 26 19.9 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
28 25 27 syl6ib ${⊢}{u}\ne {v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
29 orc ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)$
30 28 29 syl6 ${⊢}{u}\ne {v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)\right)$
31 7 30 pm2.61ine ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)$
32 5 31 impbii ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$