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

Theorem rmo4 3264
 Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.)
Hypothesis
Ref Expression
rmo4.1
Assertion
Ref Expression
rmo4
Distinct variable groups:   ,,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem rmo4
StepHypRef Expression
1 df-rmo 2783 . 2
2 an4 831 . . . . . . . . 9
3 ancom 451 . . . . . . . . . 10
43anbi1i 699 . . . . . . . . 9
52, 4bitri 252 . . . . . . . 8
65imbi1i 326 . . . . . . 7
7 impexp 447 . . . . . . 7
8 impexp 447 . . . . . . 7
96, 7, 83bitri 274 . . . . . 6
109albii 1687 . . . . 5
11 df-ral 2780 . . . . 5
12 r19.21v 2830 . . . . 5
1310, 11, 123bitr2i 276 . . . 4
1413albii 1687 . . 3
15 eleq1 2494 . . . . 5
16 rmo4.1 . . . . 5
1715, 16anbi12d 715 . . . 4
1817mo4 2313 . . 3
19 df-ral 2780 . . 3
2014, 18, 193bitr4i 280 . 2
211, 20bitri 252 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370  wal 1435   wcel 1868  wmo 2266  wral 2775  wrmo 2778 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-cleq 2414  df-clel 2417  df-ral 2780  df-rmo 2783 This theorem is referenced by:  reu4  3265  disjor  4405  somo  4804  supmo  7968  infmo  8013  sqrmo  13303  catideu  15568  poslubmo  16379  posglbmo  16380  mgmidmo  16489  lspextmo  18266  evlseu  18726  ply1divmo  23072  tghilberti2  24669  foot  24750  mideu  24766  2sqmo  28404  cvmliftmo  30002  hilbert1.2  30914  poimirlem1  31854  poimirlem13  31866  poimirlem14  31867  poimirlem18  31871  poimirlem21  31874  idomsubgmo  35991
 Copyright terms: Public domain W3C validator