Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brcolinear Structured version   Unicode version

Theorem brcolinear 29677
 Description: The binary relationship form of the colinearity predicate. (Contributed by Scott Fenton, 5-Oct-2013.)
Assertion
Ref Expression
brcolinear

Proof of Theorem brcolinear
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 brcolinear2 29676 . . . 4
4 simpr 461 . . . 4
54rexlimivw 2930 . . 3
6 fveq2 5852 . . . . . . . 8
76eleq2d 2511 . . . . . . 7
86eleq2d 2511 . . . . . . 7
96eleq2d 2511 . . . . . . 7
107, 8, 93anbi123d 1298 . . . . . 6
1110anbi1d 704 . . . . 5
1211rspcev 3194 . . . 4
1312expr 615 . . 3
145, 13impbid2 204 . 2
153, 14bitrd 253 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   w3o 971   w3a 972   wceq 1381   wcel 1802  wrex 2792  cop 4016   class class class wbr 4433  cfv 5574  cn 10537  cee 24056   cbtwn 24057   ccolin 29655 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-xp 4991  df-rel 4992  df-cnv 4993  df-iota 5537  df-fv 5582  df-oprab 6281  df-colinear 29657 This theorem is referenced by:  colinearperm1  29680  colinearperm3  29681  colineartriv1  29685  colineartriv2  29686  btwncolinear1  29687  colinearxfr  29693  lineext  29694  fscgr  29698  colinbtwnle  29736  broutsideof2  29740  lineunray  29765  lineelsb2  29766
 Copyright terms: Public domain W3C validator