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

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

Proof of Theorem reu3
StepHypRef Expression
1 reurex 2995 . . 3
2 reu6 3215 . . . 4
3 biimp 198 . . . . . 6
43ralimi 2796 . . . . 5
54reximi 2852 . . . 4
62, 5sylbi 200 . . 3
71, 6jca 541 . 2
8 rexex 2843 . . . 4
98anim2i 579 . . 3
10 eu3v 2347 . . . 4
11 df-reu 2763 . . . 4
12 df-rex 2762 . . . . 5
13 df-ral 2761 . . . . . . 7
14 impexp 453 . . . . . . . 8
1514albii 1699 . . . . . . 7
1613, 15bitr4i 260 . . . . . 6
1716exbii 1726 . . . . 5
1812, 17anbi12i 711 . . . 4
1910, 11, 183bitr4i 285 . . 3
209, 19sylibr 217 . 2
217, 20impbii 192 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376  wal 1450  wex 1671   wcel 1904  weu 2319  wral 2756  wrex 2757  wreu 2758 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-cleq 2464  df-clel 2467  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764 This theorem is referenced by:  reu7  3221  2reu4a  38755
 Copyright terms: Public domain W3C validator