Metamath Proof Explorer


Theorem ax6e2ndALT

Description: If at least two sets exist ( dtru ) , then the same is true expressed in an alternate form similar to the form of ax6e . The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2ndALT ¬ x x = y x y x = u y = v

Proof

Step Hyp Ref Expression
1 vex u V
2 ax6e y y = v
3 1 2 pm3.2i u V y y = v
4 19.42v y u V y = v u V y y = v
5 4 biimpri u V y y = v y u V y = v
6 3 5 ax-mp y u V y = v
7 isset u V x x = u
8 7 anbi1i u V y = v x x = u y = v
9 8 exbii y u V y = v y x x = u y = v
10 6 9 mpbi y x x = u y = v
11 id ¬ x x = y ¬ x x = y
12 hbnae ¬ x x = y y ¬ x x = y
13 hbn1 ¬ x x = y x ¬ x x = y
14 ax-5 z = v x z = v
15 ax-5 y = v z y = v
16 id z = y z = y
17 equequ1 z = y z = v y = v
18 17 a1i z = y z = y z = y z = v y = v
19 16 18 ax-mp z = y z = v y = v
20 14 15 19 dvelimh ¬ x x = y y = v x y = v
21 11 20 syl ¬ x x = y y = v x y = v
22 21 idiALT ¬ x x = y y = v x y = v
23 22 alimi x ¬ x x = y x y = v x y = v
24 13 23 syl ¬ x x = y x y = v x y = v
25 11 24 syl ¬ x x = y x y = v x y = v
26 19.41rg x y = v x y = v x x = u y = v x x = u y = v
27 25 26 syl ¬ x x = y x x = u y = v x x = u y = v
28 27 idiALT ¬ x x = y x x = u y = v x x = u y = v
29 28 alimi y ¬ x x = y y x x = u y = v x x = u y = v
30 12 29 syl ¬ x x = y y x x = u y = v x x = u y = v
31 11 30 syl ¬ x x = y y x x = u y = v x x = u y = v
32 exim y x x = u y = v x x = u y = v y x x = u y = v y x x = u y = v
33 31 32 syl ¬ x x = y y x x = u y = v y x x = u y = v
34 pm3.35 y x x = u y = v y x x = u y = v y x x = u y = v y x x = u y = v
35 10 33 34 sylancr ¬ x x = y y x x = u y = v
36 excomim y x x = u y = v x y x = u y = v
37 35 36 syl ¬ x x = y x y x = u y = v
38 37 idiALT ¬ x x = y x y x = u y = v