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

Theorem brrelex2i 4919
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 4917 . 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 1725   _Vcvv 2956   class class class wbr 4212   Rel wrel 4883
This theorem is referenced by:  vtoclr  4922  brdomi  7119  domdifsn  7191  undom  7196  xpdom2  7203  xpdom1g  7205  domunsncan  7208  fodomr  7258  pwdom  7259  domssex  7268  xpen  7270  mapdom1  7272  mapdom2  7278  pwen  7280  sucdom2  7303  unxpdom  7316  unxpdom2  7317  sucxpdom  7318  isfinite2  7365  infn0  7369  fin2inf  7370  card2on  7522  elharval  7531  harword  7533  brwdomi  7536  brwdomn0  7537  domwdom  7542  wdomtr  7543  wdompwdom  7546  canthwdom  7547  brwdom3i  7551  unwdomg  7552  xpwdomg  7553  unxpwdom  7557  infdifsn  7611  infdiffi  7612  isnum2  7832  wdomfil  7942  cdaen  8053  cdaenun  8054  cdadom1  8066  cdaxpdom  8069  cdainf  8072  infcda1  8073  pwcdaidm  8075  cdalepw  8076  infpss  8097  infmap2  8098  fictb  8125  infpssALT  8193  enfin2i  8201  fin34  8270  fodomb  8404  wdomac  8405  iundom2g  8415  iundom  8417  sdomsdomcard  8435  infxpidm  8437  engch  8503  fpwwe2lem3  8508  canthp1lem1  8527  canthp1lem2  8528  canthp1  8529  pwfseq  8539  pwxpndom2  8540  pwxpndom  8541  pwcdandom  8542  gchaclem  8545  hargch  8552  hasheni  11632  hashdomi  11654  brfi1uzind  11715  clim  12288  rlim  12289  ssc1  14021  ssc2  14022  ssctr  14025  frgpnabl  15486  dprdval  15561  dprdgrp  15563  dprdf  15564  dprdcntz  15566  dprddisj  15567  dprdw  15568  dprdssv  15574  dprdfid  15575  dprdfinv  15577  dprdfadd  15578  dprdfsub  15579  dprdfeq0  15580  dprdf11  15581  dprdlub  15584  dprdres  15586  dprdss  15587  dprdf1o  15590  subgdmdprd  15592  dmdprdsplitlem  15595  dprddisj2  15597  dprd2da  15600  dmdprdsplit2  15604  dpjfval  15613  dpjidcl  15616  1stcrestlem  17515  hauspwdom  17564  ufilen  17962  dvle  19891  uhgrav  21337  umgraf2  21352  umgrares  21359  umisuhgra  21362  umgraun  21363  uslgrav  21370  usgrav  21371  uslgraf  21374  iscusgra0  21466  ntrivcvgn0  25226  isfne4  26349  refbas  26360  refssex  26361  fnetr  26366  reftr  26369  topfneec  26371  fnessref  26373  refssfne  26374  enfixsn  27234  mapfien2  27235  frisusgrapr  28381
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-opab 4267  df-xp 4884  df-rel 4885
  Copyright terms: Public domain W3C validator