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

Theorem brrelex2i 4732
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 4730 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 651 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   _Vcvv 2790   class class class wbr 4025   Rel wrel 4696
This theorem is referenced by:  vtoclr  4735  brdomi  6875  domdifsn  6947  undom  6952  xpdom2  6959  xpdom1g  6961  domunsncan  6964  fodomr  7014  pwdom  7015  domssex  7024  xpen  7026  mapdom1  7028  mapdom2  7034  pwen  7036  sucdom2  7059  unxpdom  7072  unxpdom2  7073  sucxpdom  7074  isfinite2  7117  infn0  7121  fin2inf  7122  card2on  7270  elharval  7279  harword  7281  brwdomi  7284  brwdomn0  7285  domwdom  7290  wdomtr  7291  wdompwdom  7294  canthwdom  7295  brwdom3i  7299  unwdomg  7300  xpwdomg  7301  unxpwdom  7305  infdifsn  7359  infdiffi  7360  isnum2  7580  wdomfil  7690  cdaen  7801  cdaenun  7802  cdadom1  7814  cdaxpdom  7817  cdainf  7820  infcda1  7821  pwcdaidm  7823  cdalepw  7824  infpss  7845  infmap2  7846  fictb  7873  infpssALT  7941  enfin2i  7949  fin34  8018  fodomb  8153  wdomac  8154  iundom2g  8164  iundom  8166  sdomsdomcard  8184  infxpidm  8186  engch  8252  fpwwe2lem3  8257  canthp1lem1  8276  canthp1lem2  8277  canthp1  8278  pwfseq  8288  pwxpndom2  8289  pwxpndom  8290  pwcdandom  8291  gchaclem  8294  hargch  8301  hasheni  11349  hashdomi  11364  clim  11970  rlim  11971  ssc1  13700  ssc2  13701  ssctr  13704  eqgval  14668  frgpnabl  15165  dprdval  15240  dprdgrp  15242  dprdf  15243  dprdcntz  15245  dprddisj  15246  dprdw  15247  dprdssv  15253  dprdfid  15254  dprdfinv  15256  dprdfadd  15257  dprdfsub  15258  dprdfeq0  15259  dprdf11  15260  dprdlub  15263  dprdres  15265  dprdss  15266  dprdf1o  15269  subgdmdprd  15271  dmdprdsplitlem  15274  dprddisj2  15276  dprd2da  15279  dmdprdsplit2  15283  dpjfval  15292  dpjidcl  15295  1stcrestlem  17180  hauspwdom  17229  ufilen  17627  dvle  19356  umgraf2  23871  umgrares  23878  umgraun  23881  isfne4  26280  refbas  26291  refssex  26292  fnetr  26297  reftr  26300  topfneec  26302  fnessref  26304  refssfne  26305  enfixsn  27268  mapfien2  27269  uslgrav  28111  usgrav  28112  uslgraf  28115  usgrares  28126  iscusgra0  28165  frisusgrapr  28183
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-xp 4697  df-rel 4698
  Copyright terms: Public domain W3C validator