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

Theorem brel 5053
Description: Two things in a binary relation belong to the relation's domain. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
Hypothesis
Ref Expression
brel.1
Assertion
Ref Expression
brel

Proof of Theorem brel
StepHypRef Expression
1 brel.1 . . 3
21ssbri 4494 . 2
3 brxp 5035 . 2
42, 3sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  C_wss 3475   class class class wbr 4452  X.cxp 5002
This theorem is referenced by:  brab2a  5054  brab2ga  5080  soirri  5398  sotri  5399  sotri2  5401  sotri3  5402  soirriOLD  5403  sotriOLD  5404  ndmovord  6465  ndmovordi  6466  swoer  7358  brecop2  7424  ecopovsym  7432  ecopovtrn  7433  hartogslem1  7988  nlt1pi  9305  indpi  9306  nqerf  9329  ordpipq  9341  lterpq  9369  ltexnq  9374  ltbtwnnq  9377  ltrnq  9378  prnmadd  9396  genpcd  9405  nqpr  9413  1idpr  9428  ltexprlem4  9438  ltexpri  9442  ltaprlem  9443  prlem936  9446  reclem2pr  9447  reclem3pr  9448  reclem4pr  9449  suplem1pr  9451  suplem2pr  9452  supexpr  9453  recexsrlem  9501  addgt0sr  9502  mulgt0sr  9503  mappsrpr  9506  map2psrpr  9508  supsrlem  9509  supsr  9510  ltresr  9538  dfle2  11382  dflt2  11383  dvdszrcl  13991  letsr  15857  hmphtop  20279  vcex  25473  brtxp2  29531  brpprod3a  29536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010
  Copyright terms: Public domain W3C validator