ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  reu6 Structured version   Unicode version

Theorem reu6 2724
Description: A way to express restricted uniqueness. (Contributed by NM, 20-Oct-2006.)
Assertion
Ref Expression
reu6
Distinct variable groups:   ,,   ,
Allowed substitution hint:   ()

Proof of Theorem reu6
StepHypRef Expression
1 df-reu 2307 . 2
2 19.28v 1777 . . . . 5
3 eleq1 2097 . . . . . . . . . . . 12
4 sbequ12 1651 . . . . . . . . . . . 12
53, 4anbi12d 442 . . . . . . . . . . 11
6 equequ1 1595 . . . . . . . . . . 11
75, 6bibi12d 224 . . . . . . . . . 10
8 equid 1586 . . . . . . . . . . . 12
98tbt 236 . . . . . . . . . . 11
10 simpl 102 . . . . . . . . . . 11
119, 10sylbir 125 . . . . . . . . . 10
127, 11syl6bi 152 . . . . . . . . 9
1312spimv 1689 . . . . . . . 8
14 bi1 111 . . . . . . . . . . . 12
1514expdimp 246 . . . . . . . . . . 11
16 bi2 121 . . . . . . . . . . . . 13
17 simpr 103 . . . . . . . . . . . . 13
1816, 17syl6 29 . . . . . . . . . . . 12
1918adantr 261 . . . . . . . . . . 11
2015, 19impbid 120 . . . . . . . . . 10
2120ex 108 . . . . . . . . 9
2221sps 1427 . . . . . . . 8
2313, 22jca 290 . . . . . . 7
2423a5i 1432 . . . . . 6
25 bi1 111 . . . . . . . . . . 11
2625imim2i 12 . . . . . . . . . 10
2726impd 242 . . . . . . . . 9
2827adantl 262 . . . . . . . 8
29 eleq1a 2106 . . . . . . . . . . . 12
3029adantr 261 . . . . . . . . . . 11
3130imp 115 . . . . . . . . . 10
32 bi2 121 . . . . . . . . . . . . . 14
3332imim2i 12 . . . . . . . . . . . . 13
3433com23 72 . . . . . . . . . . . 12
3534imp 115 . . . . . . . . . . 11
3635adantll 445 . . . . . . . . . 10
3731, 36jcai 294 . . . . . . . . 9
3837ex 108 . . . . . . . 8
3928, 38impbid 120 . . . . . . 7
4039alimi 1341 . . . . . 6
4124, 40impbii 117 . . . . 5
42 df-ral 2305 . . . . . 6
4342anbi2i 430 . . . . 5
442, 41, 433bitr4i 201 . . . 4
4544exbii 1493 . . 3
46 df-eu 1900 . . 3
47 df-rex 2306 . . 3
4845, 46, 473bitr4i 201 . 2
491, 48bitri 173 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98  wal 1240  wex 1378   wcel 1390  wsb 1642  weu 1897  wral 2300  wrex 2301  wreu 2302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-eu 1900  df-cleq 2030  df-clel 2033  df-ral 2305  df-rex 2306  df-reu 2307
This theorem is referenced by:  reu3  2725  reu6i  2726  reu8  2731
  Copyright terms: Public domain W3C validator