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

Theorem brrelex2i 4955
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 4953 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 668 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   _Vcvv 3034   class class class wbr 4367   Rel wrel 4918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920
This theorem is referenced by:  vtoclr  4958  brdomi  7446  domdifsn  7519  undom  7524  xpdom2  7531  xpdom1g  7533  domunsncan  7536  enfixsn  7545  fodomr  7587  pwdom  7588  domssex  7597  xpen  7599  mapdom1  7601  mapdom2  7607  pwen  7609  sucdom2  7632  unxpdom  7643  unxpdom2  7644  sucxpdom  7645  isfinite2  7693  infn0  7697  fin2inf  7698  fsuppimp  7750  suppeqfsuppbi  7758  fsuppsssupp  7760  fsuppunbi  7765  funsnfsupp  7768  mapfien2  7783  wemapso2  7894  card2on  7895  elharval  7904  harword  7906  brwdomi  7909  brwdomn0  7910  domwdom  7915  wdomtr  7916  wdompwdom  7919  canthwdom  7920  brwdom3i  7924  unwdomg  7925  xpwdomg  7926  unxpwdom  7930  infdifsn  7987  infdiffi  7988  isnum2  8239  wdomfil  8355  cdaen  8466  cdaenun  8467  cdadom1  8479  cdaxpdom  8482  cdainf  8485  infcda1  8486  pwcdaidm  8488  cdalepw  8489  infpss  8510  infmap2  8511  fictb  8538  infpssALT  8606  enfin2i  8614  fin34  8683  fodomb  8817  wdomac  8818  iundom2g  8828  iundom  8830  sdomsdomcard  8848  infxpidm  8850  engch  8917  fpwwe2lem3  8922  canthp1lem1  8941  canthp1lem2  8942  canthp1  8943  pwfseq  8953  pwxpndom2  8954  pwxpndom  8955  pwcdandom  8956  hargch  8962  gchaclem  8967  hasheni  12323  hashdomi  12351  brfi1uzind  12436  clim  13319  rlim  13320  ntrivcvgn0  13709  ssc1  15227  ssc2  15228  ssctr  15231  frgpnabl  16996  dprddomprc  17144  dprdval  17147  dprdvalOLD  17149  dprdgrp  17151  dprdf  17152  dprdwOLD  17163  dprdssv  17169  dprdfidOLD  17177  dprdfinvOLD  17179  dprdfaddOLD  17180  dprdfsubOLD  17181  dprdfeq0OLD  17182  dprdf11OLD  17183  subgdmdprd  17194  dmdprdsplitlemOLD  17198  dprddisj2OLD  17201  dprd2da  17204  dpjidclOLD  17227  1stcrestlem  20038  hauspwdom  20087  isref  20095  ufilen  20516  dvle  22493  uhgrav  24417  ushgraf  24423  ushgrauhgra  24424  umgraf2  24438  umgrares  24445  umisuhgra  24448  umgraun  24449  uslgrav  24458  usgrav  24459  uslgraf  24466  iscusgra0  24578  frisusgrapr  25112  locfinref  27998  isfne4  30324  fnetr  30335  topfneec  30339  fnessref  30341  refssfne  30342  mapfien2OLD  31208  climf  31794  linindsv  33246
  Copyright terms: Public domain W3C validator