Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rmo4fOLD Structured version   Unicode version

Theorem rmo4fOLD 27796
 Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by Thierry Arnoux, 11-Oct-2016.) (Revised by Thierry Arnoux, 8-Mar-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
rmo4f.1
rmo4f.2
rmo4f.3
rmo4f.4
Assertion
Ref Expression
rmo4fOLD
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   (,)   (,)

Proof of Theorem rmo4fOLD
StepHypRef Expression
1 an4 825 . . . . . . . 8
2 ancom 448 . . . . . . . . 9
32anbi1i 693 . . . . . . . 8
41, 3bitri 249 . . . . . . 7
54imbi1i 323 . . . . . 6
6 impexp 444 . . . . . 6
7 impexp 444 . . . . . 6
85, 6, 73bitri 271 . . . . 5
98albii 1661 . . . 4
10 df-ral 2758 . . . 4
11 nfcv 2564 . . . . . 6
12 rmo4f.2 . . . . . 6
1311, 12nfel 2577 . . . . 5
1413r19.21 2802 . . . 4
159, 10, 143bitr2i 273 . . 3
1615albii 1661 . 2
17 nfv 1728 . . . . 5
1813, 17nfan 1956 . . . 4
1918mo3 2278 . . 3
20 nfcv 2564 . . . . . . . . 9
21 rmo4f.1 . . . . . . . . 9
2220, 21nfel 2577 . . . . . . . 8
23 rmo4f.3 . . . . . . . 8
2422, 23nfan 1956 . . . . . . 7
25 eleq1 2474 . . . . . . . 8
26 rmo4f.4 . . . . . . . 8
2725, 26anbi12d 709 . . . . . . 7
2824, 27sbie 2173 . . . . . 6
2928anbi2i 692 . . . . 5
3029imbi1i 323 . . . 4
31302albii 1662 . . 3
3219, 31bitri 249 . 2
33 df-ral 2758 . 2
3416, 32, 333bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 367  wal 1403   wceq 1405  wnf 1637  wsb 1763   wcel 1842  wmo 2239  wnfc 2550  wral 2753 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380 This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator