Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  euind Structured version   Unicode version

Theorem euind 3123
 Description: Existential uniqueness via an indirect equality. (Contributed by NM, 11-Oct-2010.)
Hypotheses
Ref Expression
euind.1
euind.2
euind.3
Assertion
Ref Expression
euind
Distinct variable groups:   ,,   ,,   ,,   ,,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem euind
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 euind.2 . . . . . 6
21cbvexv 1986 . . . . 5
3 euind.1 . . . . . . . . 9
43isseti 2964 . . . . . . . 8
54biantrur 494 . . . . . . 7
65exbii 1593 . . . . . 6
7 19.41v 1925 . . . . . . 7
87exbii 1593 . . . . . 6
9 excom 1757 . . . . . 6
106, 8, 93bitr2i 266 . . . . 5
112, 10bitri 242 . . . 4
12 eqeq2 2447 . . . . . . . . 9
1312imim2i 14 . . . . . . . 8
14 bi2 191 . . . . . . . . . 10
1514imim2i 14 . . . . . . . . 9
16 an31 777 . . . . . . . . . . 11
1716imbi1i 317 . . . . . . . . . 10
18 impexp 435 . . . . . . . . . 10
19 impexp 435 . . . . . . . . . 10
2017, 18, 193bitr3i 268 . . . . . . . . 9
2115, 20sylib 190 . . . . . . . 8
2213, 21syl 16 . . . . . . 7
23222alimi 1570 . . . . . 6
24 19.23v 1915 . . . . . . . 8
2524albii 1576 . . . . . . 7
26 19.21v 1914 . . . . . . 7
2725, 26bitri 242 . . . . . 6
2823, 27sylib 190 . . . . 5
2928eximdv 1633 . . . 4
3011, 29syl5bi 210 . . 3
3130imp 420 . 2
32 pm4.24 626 . . . . . . . 8
3332biimpi 188 . . . . . . 7
34 prth 556 . . . . . . 7
35 eqtr3 2457 . . . . . . 7
3633, 34, 35syl56 33 . . . . . 6
3736alanimi 1572 . . . . 5
38 19.23v 1915 . . . . . . 7
3938biimpi 188 . . . . . 6
4039com12 30 . . . . 5
4137, 40syl5 31 . . . 4
4241alrimivv 1643 . . 3