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

Theorem brrelex2i 4859
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 4857 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 652 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   _Vcvv 2899   class class class wbr 4153   Rel wrel 4823
This theorem is referenced by:  vtoclr  4862  brdomi  7055  domdifsn  7127  undom  7132  xpdom2  7139  xpdom1g  7141  domunsncan  7144  fodomr  7194  pwdom  7195  domssex  7204  xpen  7206  mapdom1  7208  mapdom2  7214  pwen  7216  sucdom2  7239  unxpdom  7252  unxpdom2  7253  sucxpdom  7254  isfinite2  7301  infn0  7305  fin2inf  7306  card2on  7455  elharval  7464  harword  7466  brwdomi  7469  brwdomn0  7470  domwdom  7475  wdomtr  7476  wdompwdom  7479  canthwdom  7480  brwdom3i  7484  unwdomg  7485  xpwdomg  7486  unxpwdom  7490  infdifsn  7544  infdiffi  7545  isnum2  7765  wdomfil  7875  cdaen  7986  cdaenun  7987  cdadom1  7999  cdaxpdom  8002  cdainf  8005  infcda1  8006  pwcdaidm  8008  cdalepw  8009  infpss  8030  infmap2  8031  fictb  8058  infpssALT  8126  enfin2i  8134  fin34  8203  fodomb  8337  wdomac  8338  iundom2g  8348  iundom  8350  sdomsdomcard  8368  infxpidm  8370  engch  8436  fpwwe2lem3  8441  canthp1lem1  8460  canthp1lem2  8461  canthp1  8462  pwfseq  8472  pwxpndom2  8473  pwxpndom  8474  pwcdandom  8475  gchaclem  8478  hargch  8485  hasheni  11559  hashdomi  11581  brfi1uzind  11642  clim  12215  rlim  12216  ssc1  13948  ssc2  13949  ssctr  13952  frgpnabl  15413  dprdval  15488  dprdgrp  15490  dprdf  15491  dprdcntz  15493  dprddisj  15494  dprdw  15495  dprdssv  15501  dprdfid  15502  dprdfinv  15504  dprdfadd  15505  dprdfsub  15506  dprdfeq0  15507  dprdf11  15508  dprdlub  15511  dprdres  15513  dprdss  15514  dprdf1o  15517  subgdmdprd  15519  dmdprdsplitlem  15522  dprddisj2  15524  dprd2da  15527  dmdprdsplit2  15531  dpjfval  15540  dpjidcl  15543  1stcrestlem  17436  hauspwdom  17485  ufilen  17883  dvle  19758  uhgrav  21204  umgraf2  21219  umgrares  21226  umisuhgra  21229  umgraun  21230  uslgrav  21237  usgrav  21238  uslgraf  21241  iscusgra0  21332  ntrivcvgn0  25005  isfne4  26040  refbas  26051  refssex  26052  fnetr  26057  reftr  26060  topfneec  26062  fnessref  26064  refssfne  26065  enfixsn  26926  mapfien2  26927  frisusgrapr  27744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-br 4154  df-opab 4208  df-xp 4824  df-rel 4825
  Copyright terms: Public domain W3C validator