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

Theorem brrelex2i 4730
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 4728 . 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 1684   _Vcvv 2788   class class class wbr 4023   Rel wrel 4694
This theorem is referenced by:  vtoclr  4733  brdomi  6873  domdifsn  6945  undom  6950  xpdom2  6957  xpdom1g  6959  domunsncan  6962  fodomr  7012  pwdom  7013  domssex  7022  xpen  7024  mapdom1  7026  mapdom2  7032  pwen  7034  sucdom2  7057  unxpdom  7070  unxpdom2  7071  sucxpdom  7072  isfinite2  7115  infn0  7119  fin2inf  7120  card2on  7268  elharval  7277  harword  7279  brwdomi  7282  brwdomn0  7283  domwdom  7288  wdomtr  7289  wdompwdom  7292  canthwdom  7293  brwdom3i  7297  unwdomg  7298  xpwdomg  7299  unxpwdom  7303  infdifsn  7357  infdiffi  7358  isnum2  7578  wdomfil  7688  cdaen  7799  cdaenun  7800  cdadom1  7812  cdaxpdom  7815  cdainf  7818  infcda1  7819  pwcdaidm  7821  cdalepw  7822  infpss  7843  infmap2  7844  fictb  7871  infpssALT  7939  enfin2i  7947  fin34  8016  fodomb  8151  wdomac  8152  iundom2g  8162  iundom  8164  sdomsdomcard  8182  infxpidm  8184  engch  8250  fpwwe2lem3  8255  canthp1lem1  8274  canthp1lem2  8275  canthp1  8276  pwfseq  8286  pwxpndom2  8287  pwxpndom  8288  pwcdandom  8289  gchaclem  8292  hargch  8299  hasheni  11347  hashdomi  11362  clim  11968  rlim  11969  ssc1  13698  ssc2  13699  ssctr  13702  eqgval  14666  frgpnabl  15163  dprdval  15238  dprdgrp  15240  dprdf  15241  dprdcntz  15243  dprddisj  15244  dprdw  15245  dprdssv  15251  dprdfid  15252  dprdfinv  15254  dprdfadd  15255  dprdfsub  15256  dprdfeq0  15257  dprdf11  15258  dprdlub  15261  dprdres  15263  dprdss  15264  dprdf1o  15267  subgdmdprd  15269  dmdprdsplitlem  15272  dprddisj2  15274  dprd2da  15277  dmdprdsplit2  15281  dpjfval  15290  dpjidcl  15293  1stcrestlem  17178  hauspwdom  17227  ufilen  17625  dvle  19354  umgraf2  23869  umgrares  23876  umgraun  23879  isfne4  26269  refbas  26280  refssex  26281  fnetr  26286  reftr  26289  topfneec  26291  fnessref  26293  refssfne  26294  enfixsn  27257  mapfien2  27258  uslgrav  28100  usgrav  28101  uslgraf  28104  usgrares  28115  iscusgra0  28154  frisusgrapr  28172
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-xp 4695  df-rel 4696
  Copyright terms: Public domain W3C validator