# Metamath Proof Explorer

## Theorem ax6e2ndeqALT

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 . Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2ndeqALT ${⊢}\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 exmid ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
5 jao ${⊢}\left(\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)\right)\to \left(\left(¬\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)\right)\to \left(\left(\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\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)\right)\right)$
6 5 3imp ${⊢}\left(\left(\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)\right)\wedge \left(¬\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)\right)\wedge \left(\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\right)\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)$
7 2 3 4 6 mp3an ${⊢}{u}={v}\to \exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)$
8 1 7 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)$
9 hbnae ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
10 9 eximi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
11 nfa1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
12 11 19.9 ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
13 10 12 sylib ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
14 sp ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
15 13 14 syl ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
16 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)$
17 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
18 17 nfn ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
19 18 19.9 ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
20 id ${⊢}{u}\ne {v}\to {u}\ne {v}$
21 simpr ${⊢}\left({u}\ne {v}\wedge \left({x}={u}\wedge {y}={v}\right)\right)\to \left({x}={u}\wedge {y}={v}\right)$
22 simpl ${⊢}\left({x}={u}\wedge {y}={v}\right)\to {x}={u}$
23 21 22 syl ${⊢}\left({u}\ne {v}\wedge \left({x}={u}\wedge {y}={v}\right)\right)\to {x}={u}$
24 pm13.181 ${⊢}\left({x}={u}\wedge {u}\ne {v}\right)\to {x}\ne {v}$
25 24 ancoms ${⊢}\left({u}\ne {v}\wedge {x}={u}\right)\to {x}\ne {v}$
26 20 23 25 syl2an2r ${⊢}\left({u}\ne {v}\wedge \left({x}={u}\wedge {y}={v}\right)\right)\to {x}\ne {v}$
27 simpr ${⊢}\left({x}={u}\wedge {y}={v}\right)\to {y}={v}$
28 21 27 syl ${⊢}\left({u}\ne {v}\wedge \left({x}={u}\wedge {y}={v}\right)\right)\to {y}={v}$
29 neeq2 ${⊢}{y}={v}\to \left({x}\ne {y}↔{x}\ne {v}\right)$
30 29 biimparc ${⊢}\left({x}\ne {v}\wedge {y}={v}\right)\to {x}\ne {y}$
31 26 28 30 syl2anc ${⊢}\left({u}\ne {v}\wedge \left({x}={u}\wedge {y}={v}\right)\right)\to {x}\ne {y}$
32 df-ne ${⊢}{x}\ne {y}↔¬{x}={y}$
33 32 bicomi ${⊢}¬{x}={y}↔{x}\ne {y}$
34 sp ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to {x}={y}$
35 34 con3i ${⊢}¬{x}={y}\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
36 33 35 sylbir ${⊢}{x}\ne {y}\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
37 31 36 syl ${⊢}\left({u}\ne {v}\wedge \left({x}={u}\wedge {y}={v}\right)\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
38 37 ex ${⊢}{u}\ne {v}\to \left(\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
39 38 alrimiv ${⊢}{u}\ne {v}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
40 exim ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\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)$
41 39 40 syl ${⊢}{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)$
42 imbi2 ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \left(\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)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\right)$
43 42 biimpa ${⊢}\left(\left(\exists {x}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\wedge \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)\right)\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)$
44 19 41 43 sylancr ${⊢}{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)$
45 44 alrimiv ${⊢}{u}\ne {v}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)$
46 exim ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\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)$
47 45 46 syl ${⊢}{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)$
48 imbi1 ${⊢}\left(\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)\right)\to \left(\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)↔\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)\right)$
49 48 biimpar ${⊢}\left(\left(\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)\right)\wedge \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)\right)\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)$
50 16 47 49 sylancr ${⊢}{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)$
51 pm3.34 ${⊢}\left(\left(\exists {y}\phantom{\rule{.4em}{0ex}}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\wedge \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)\right)\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)$
52 15 50 51 sylancr ${⊢}{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)$
53 orc ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)$
54 53 imim2i ${⊢}\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)\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)$
55 52 54 syl ${⊢}{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)$
56 55 idiALT ${⊢}{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)$
57 id ${⊢}{u}={v}\to {u}={v}$
58 ax-1 ${⊢}{u}={v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to {u}={v}\right)$
59 57 58 syl ${⊢}{u}={v}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to {u}={v}\right)$
60 olc ${⊢}{u}={v}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\vee {u}={v}\right)$
61 60 imim2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}={u}\wedge {y}={v}\right)\to {u}={v}\right)\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)$
62 59 61 syl ${⊢}{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)$
63 62 idiALT ${⊢}{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)$
64 exmidne ${⊢}\left({u}={v}\vee {u}\ne {v}\right)$
65 jao ${⊢}\left({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)\right)\to \left(\left({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)\right)\to \left(\left({u}={v}\vee {u}\ne {v}\right)\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)\right)\right)$
66 65 3imp21 ${⊢}\left(\left({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)\right)\wedge \left({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)\right)\wedge \left({u}={v}\vee {u}\ne {v}\right)\right)\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)$
67 56 63 64 66 mp3an ${⊢}\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)$
68 8 67 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)$