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

Theorem brrelex2i 4895
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 4893 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 674 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   _Vcvv 3080   class class class wbr 4423   Rel wrel 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-br 4424  df-opab 4483  df-xp 4859  df-rel 4860
This theorem is referenced by:  vtoclr  4898  brdomi  7591  domdifsn  7664  undom  7669  xpdom2  7676  xpdom1g  7678  domunsncan  7681  enfixsn  7690  fodomr  7732  pwdom  7733  domssex  7742  xpen  7744  mapdom1  7746  mapdom2  7752  pwen  7754  sucdom2  7777  unxpdom  7788  unxpdom2  7789  sucxpdom  7790  isfinite2  7838  infn0  7842  fin2inf  7843  fsuppimp  7898  suppeqfsuppbi  7906  fsuppsssupp  7908  fsuppunbi  7913  funsnfsupp  7916  mapfien2  7931  wemapso2  8077  card2on  8078  elharval  8087  harword  8089  brwdomi  8092  brwdomn0  8093  domwdom  8098  wdomtr  8099  wdompwdom  8102  canthwdom  8103  brwdom3i  8107  unwdomg  8108  xpwdomg  8109  unxpwdom  8113  infdifsn  8170  infdiffi  8171  isnum2  8387  wdomfil  8499  cdaen  8610  cdaenun  8611  cdadom1  8623  cdaxpdom  8626  cdainf  8629  infcda1  8630  pwcdaidm  8632  cdalepw  8633  infpss  8654  infmap2  8655  fictb  8682  infpssALT  8750  enfin2i  8758  fin34  8827  fodomb  8961  wdomac  8962  iundom2g  8972  iundom  8974  sdomsdomcard  8992  infxpidm  8994  engch  9060  fpwwe2lem3  9065  canthp1lem1  9084  canthp1lem2  9085  canthp1  9086  pwfseq  9096  pwxpndom2  9097  pwxpndom  9098  pwcdandom  9099  hargch  9105  gchaclem  9110  hasheni  12537  hashdomi  12565  brfi1indALT  12657  clim  13557  rlim  13558  ntrivcvgn0  13953  ssc1  15725  ssc2  15726  ssctr  15729  frgpnabl  17510  dprddomprc  17631  dprdval  17634  dprdgrp  17636  dprdf  17637  dprdssv  17648  subgdmdprd  17666  dprd2da  17674  1stcrestlem  20465  hauspwdom  20514  isref  20522  ufilen  20943  dvle  22957  uhgrav  25021  ushgraf  25027  ushgrauhgra  25028  umgraf2  25042  umgrares  25049  umisuhgra  25052  umgraun  25053  uslgrav  25062  usgrav  25063  uslgraf  25070  iscusgra0  25183  frisusgrapr  25717  locfinref  28676  isfne4  31001  fnetr  31012  topfneec  31016  fnessref  31018  refssfne  31019  phpreu  31893  climf  37642  subgrv  39116  linindsv  39860
  Copyright terms: Public domain W3C validator