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

Theorem brrelex2i 4896
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 4894 . 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 1870   _Vcvv 3087   class class class wbr 4426   Rel wrel 4859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-xp 4860  df-rel 4861
This theorem is referenced by:  vtoclr  4899  brdomi  7588  domdifsn  7661  undom  7666  xpdom2  7673  xpdom1g  7675  domunsncan  7678  enfixsn  7687  fodomr  7729  pwdom  7730  domssex  7739  xpen  7741  mapdom1  7743  mapdom2  7749  pwen  7751  sucdom2  7774  unxpdom  7785  unxpdom2  7786  sucxpdom  7787  isfinite2  7835  infn0  7839  fin2inf  7840  fsuppimp  7895  suppeqfsuppbi  7903  fsuppsssupp  7905  fsuppunbi  7910  funsnfsupp  7913  mapfien2  7928  wemapso2  8068  card2on  8069  elharval  8078  harword  8080  brwdomi  8083  brwdomn0  8084  domwdom  8089  wdomtr  8090  wdompwdom  8093  canthwdom  8094  brwdom3i  8098  unwdomg  8099  xpwdomg  8100  unxpwdom  8104  infdifsn  8161  infdiffi  8162  isnum2  8378  wdomfil  8490  cdaen  8601  cdaenun  8602  cdadom1  8614  cdaxpdom  8617  cdainf  8620  infcda1  8621  pwcdaidm  8623  cdalepw  8624  infpss  8645  infmap2  8646  fictb  8673  infpssALT  8741  enfin2i  8749  fin34  8818  fodomb  8952  wdomac  8953  iundom2g  8963  iundom  8965  sdomsdomcard  8983  infxpidm  8985  engch  9052  fpwwe2lem3  9057  canthp1lem1  9076  canthp1lem2  9077  canthp1  9078  pwfseq  9088  pwxpndom2  9089  pwxpndom  9090  pwcdandom  9091  hargch  9097  gchaclem  9102  hasheni  12528  hashdomi  12556  brfi1uzind  12641  clim  13536  rlim  13537  ntrivcvgn0  13932  ssc1  15668  ssc2  15669  ssctr  15672  frgpnabl  17437  dprddomprc  17558  dprdval  17561  dprdgrp  17563  dprdf  17564  dprdssv  17575  subgdmdprd  17593  dprd2da  17601  1stcrestlem  20389  hauspwdom  20438  isref  20446  ufilen  20867  dvle  22827  uhgrav  24860  ushgraf  24866  ushgrauhgra  24867  umgraf2  24881  umgrares  24888  umisuhgra  24891  umgraun  24892  uslgrav  24901  usgrav  24902  uslgraf  24909  iscusgra0  25021  frisusgrapr  25555  locfinref  28498  isfne4  30772  fnetr  30783  topfneec  30787  fnessref  30789  refssfne  30790  phpreu  31623  climf  37264  linindsv  38988
  Copyright terms: Public domain W3C validator