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

Theorem brrelex2i 4898
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 4896 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 681 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   _Vcvv 3057   class class class wbr 4418   Rel wrel 4861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pr 4656
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4419  df-opab 4478  df-xp 4862  df-rel 4863
This theorem is referenced by:  vtoclr  4901  brdomi  7611  domdifsn  7686  undom  7691  xpdom2  7698  xpdom1g  7700  domunsncan  7703  enfixsn  7712  fodomr  7754  pwdom  7755  domssex  7764  xpen  7766  mapdom1  7768  mapdom2  7774  pwen  7776  sucdom2  7799  unxpdom  7810  unxpdom2  7811  sucxpdom  7812  isfinite2  7860  infn0  7864  fin2inf  7865  fsuppimp  7920  suppeqfsuppbi  7928  fsuppsssupp  7930  fsuppunbi  7935  funsnfsupp  7938  mapfien2  7953  wemapso2  8099  card2on  8100  elharval  8109  harword  8111  brwdomi  8114  brwdomn0  8115  domwdom  8120  wdomtr  8121  wdompwdom  8124  canthwdom  8125  brwdom3i  8129  unwdomg  8130  xpwdomg  8131  unxpwdom  8135  infdifsn  8193  infdiffi  8194  isnum2  8410  wdomfil  8523  cdaen  8634  cdaenun  8635  cdadom1  8647  cdaxpdom  8650  cdainf  8653  infcda1  8654  pwcdaidm  8656  cdalepw  8657  infpss  8678  infmap2  8679  fictb  8706  infpssALT  8774  enfin2i  8782  fin34  8851  fodomb  8985  wdomac  8986  iundom2g  8996  iundom  8998  sdomsdomcard  9016  infxpidm  9018  engch  9084  fpwwe2lem3  9089  canthp1lem1  9108  canthp1lem2  9109  canthp1  9110  pwfseq  9120  pwxpndom2  9121  pwxpndom  9122  pwcdandom  9123  hargch  9129  gchaclem  9134  hasheni  12569  hashdomi  12597  brfi1indALT  12692  clim  13613  rlim  13614  ntrivcvgn0  14009  ssc1  15781  ssc2  15782  ssctr  15785  frgpnabl  17566  dprddomprc  17687  dprdval  17690  dprdgrp  17692  dprdf  17693  dprdssv  17704  subgdmdprd  17722  dprd2da  17730  1stcrestlem  20522  hauspwdom  20571  isref  20579  ufilen  21000  dvle  23015  uhgrav  25079  ushgraf  25085  ushgrauhgra  25086  umgraf2  25100  umgrares  25107  umisuhgra  25110  umgraun  25111  uslgrav  25120  usgrav  25121  uslgraf  25128  iscusgra0  25241  frisusgrapr  25775  locfinref  28719  isfne4  31046  fnetr  31057  topfneec  31061  fnessref  31063  refssfne  31064  phpreu  31975  climf  37788  subgrv  39488  linindsv  40607
  Copyright terms: Public domain W3C validator