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

Theorem 2reu5lem3 2947
 Description: Lemma for 2reu5 2948. This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 3051. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
Assertion
Ref Expression
2reu5lem3
Distinct variable groups:   ,,,   ,,,   ,   ,,
Allowed substitution hints:   (,)   ()   ()

Proof of Theorem 2reu5lem3
StepHypRef Expression
1 2reu5lem1 2945 . . 3
2 2reu5lem2 2946 . . 3
31, 2anbi12i 681 . 2
4 2eu5 2202 . 2
5 3anass 943 . . . . . . 7
65exbii 1580 . . . . . 6
7 19.42v 2039 . . . . . 6
8 df-rex 2524 . . . . . . . 8
98bicomi 195 . . . . . . 7
109anbi2i 678 . . . . . 6
116, 7, 103bitri 264 . . . . 5
1211exbii 1580 . . . 4
13 df-rex 2524 . . . 4
1412, 13bitr4i 245 . . 3
15 3anan12 952 . . . . . . . . . . 11
1615imbi1i 317 . . . . . . . . . 10
17 impexp 435 . . . . . . . . . 10
18 impexp 435 . . . . . . . . . . 11
1918imbi2i 305 . . . . . . . . . 10
2016, 17, 193bitri 264 . . . . . . . . 9
2120albii 1554 . . . . . . . 8
22 df-ral 2523 . . . . . . . 8
23 r19.21v 2605 . . . . . . . 8
2421, 22, 233bitr2i 266 . . . . . . 7
2524albii 1554 . . . . . 6
26 df-ral 2523 . . . . . 6
2725, 26bitr4i 245 . . . . 5
2827exbii 1580 . . . 4
2928exbii 1580 . . 3
3014, 29anbi12i 681 . 2
313, 4, 303bitri 264 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178   wa 360   w3a 939  wal 1532  wex 1537   wcel 1621  weu 2118  wmo 2119  wral 2518  wrex 2519  wreu 2520  wrmo 2521 This theorem is referenced by:  2reu5  2948 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-ral 2523  df-rex 2524  df-reu 2525  df-rmo 2526
 Copyright terms: Public domain W3C validator