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

Theorem brrelex2i 5035
Description: The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)
Hypothesis
Ref Expression
brrelexi.1  |-  Rel  R
Assertion
Ref Expression
brrelex2i  |-  ( A R B  ->  B  e.  _V )

Proof of Theorem brrelex2i
StepHypRef Expression
1 brrelexi.1 . 2  |-  Rel  R
2 brrelex2 5033 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 670 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   _Vcvv 3108   class class class wbr 4442   Rel wrel 4999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-rab 2818  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-br 4443  df-opab 4501  df-xp 5000  df-rel 5001
This theorem is referenced by:  vtoclr  5038  brdomi  7519  domdifsn  7592  undom  7597  xpdom2  7604  xpdom1g  7606  domunsncan  7609  enfixsn  7618  fodomr  7660  pwdom  7661  domssex  7670  xpen  7672  mapdom1  7674  mapdom2  7680  pwen  7682  sucdom2  7706  unxpdom  7719  unxpdom2  7720  sucxpdom  7721  isfinite2  7769  infn0  7773  fin2inf  7774  fsuppimp  7826  suppeqfsuppbi  7834  fsuppsssupp  7836  fsuppunbi  7841  funsnfsupp  7844  mapfien2  7859  wemapso2  7970  card2on  7971  elharval  7980  harword  7982  brwdomi  7985  brwdomn0  7986  domwdom  7991  wdomtr  7992  wdompwdom  7995  canthwdom  7996  brwdom3i  8000  unwdomg  8001  xpwdomg  8002  unxpwdom  8006  infdifsn  8064  infdiffi  8065  isnum2  8317  wdomfil  8433  cdaen  8544  cdaenun  8545  cdadom1  8557  cdaxpdom  8560  cdainf  8563  infcda1  8564  pwcdaidm  8566  cdalepw  8567  infpss  8588  infmap2  8589  fictb  8616  infpssALT  8684  enfin2i  8692  fin34  8761  fodomb  8895  wdomac  8896  iundom2g  8906  iundom  8908  sdomsdomcard  8926  infxpidm  8928  engch  8997  fpwwe2lem3  9002  canthp1lem1  9021  canthp1lem2  9022  canthp1  9023  pwfseq  9033  pwxpndom2  9034  pwxpndom  9035  pwcdandom  9036  hargch  9042  gchaclem  9047  hasheni  12378  hashdomi  12405  brfi1uzind  12487  clim  13268  rlim  13269  ssc1  15042  ssc2  15043  ssctr  15046  frgpnabl  16665  dprddomprc  16817  dprdval  16820  dprdvalOLD  16822  dprdgrp  16824  dprdf  16825  dprdcntz  16827  dprddisj  16828  dprdw  16829  dprdwOLD  16835  dprdssv  16841  dprdfeq0  16847  dprdf11  16848  dprdfidOLD  16849  dprdfinvOLD  16851  dprdfaddOLD  16852  dprdfsubOLD  16853  dprdfeq0OLD  16854  dprdf11OLD  16855  dprdres  16860  dprdf1o  16864  subgdmdprd  16866  dmdprdsplitlemOLD  16870  dprddisj2OLD  16873  dprd2da  16876  dmdprdsplit2  16880  dpjfval  16889  dpjidclOLD  16899  1stcrestlem  19714  hauspwdom  19763  ufilen  20161  dvle  22138  uhgrav  23964  umgraf2  23982  umgrares  23989  umisuhgra  23992  umgraun  23993  uslgrav  24002  usgrav  24003  uslgraf  24010  iscusgra0  24121  frisusgrapr  24655  ntrivcvgn0  28597  isfne4  29730  refbas  29741  refssex  29742  fnetr  29747  reftr  29750  topfneec  29752  fnessref  29754  refssfne  29755  mapfien2OLD  30637  climf  31121  linindsv  31996
  Copyright terms: Public domain W3C validator