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

Theorem brrelex2i 4980
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 4978 . 2  |-  ( ( Rel  R  /\  A R B )  ->  B  e.  _V )
31, 2mpan 670 1  |-  ( A R B  ->  B  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   _Vcvv 3070   class class class wbr 4392   Rel wrel 4945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pr 4631
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-sn 3978  df-pr 3980  df-op 3984  df-br 4393  df-opab 4451  df-xp 4946  df-rel 4947
This theorem is referenced by:  vtoclr  4983  brdomi  7423  domdifsn  7496  undom  7501  xpdom2  7508  xpdom1g  7510  domunsncan  7513  enfixsn  7522  fodomr  7564  pwdom  7565  domssex  7574  xpen  7576  mapdom1  7578  mapdom2  7584  pwen  7586  sucdom2  7610  unxpdom  7623  unxpdom2  7624  sucxpdom  7625  isfinite2  7673  infn0  7677  fin2inf  7678  fsuppimp  7729  suppeqfsuppbi  7737  fsuppsssupp  7739  fsuppunbi  7744  funsnfsupp  7747  mapfien2  7761  wemapso2  7871  card2on  7872  elharval  7881  harword  7883  brwdomi  7886  brwdomn0  7887  domwdom  7892  wdomtr  7893  wdompwdom  7896  canthwdom  7897  brwdom3i  7901  unwdomg  7902  xpwdomg  7903  unxpwdom  7907  infdifsn  7965  infdiffi  7966  isnum2  8218  wdomfil  8334  cdaen  8445  cdaenun  8446  cdadom1  8458  cdaxpdom  8461  cdainf  8464  infcda1  8465  pwcdaidm  8467  cdalepw  8468  infpss  8489  infmap2  8490  fictb  8517  infpssALT  8585  enfin2i  8593  fin34  8662  fodomb  8796  wdomac  8797  iundom2g  8807  iundom  8809  sdomsdomcard  8827  infxpidm  8829  engch  8898  fpwwe2lem3  8903  canthp1lem1  8922  canthp1lem2  8923  canthp1  8924  pwfseq  8934  pwxpndom2  8935  pwxpndom  8936  pwcdandom  8937  hargch  8943  gchaclem  8948  hasheni  12222  hashdomi  12247  brfi1uzind  12323  clim  13076  rlim  13077  ssc1  14838  ssc2  14839  ssctr  14842  frgpnabl  16459  dprddomprc  16589  dprdval  16592  dprdvalOLD  16594  dprdgrp  16596  dprdf  16597  dprdcntz  16599  dprddisj  16600  dprdw  16601  dprdwOLD  16607  dprdssv  16613  dprdfeq0  16619  dprdf11  16620  dprdfidOLD  16621  dprdfinvOLD  16623  dprdfaddOLD  16624  dprdfsubOLD  16625  dprdfeq0OLD  16626  dprdf11OLD  16627  dprdres  16632  dprdf1o  16636  subgdmdprd  16638  dmdprdsplitlemOLD  16642  dprddisj2OLD  16645  dprd2da  16648  dmdprdsplit2  16652  dpjfval  16661  dpjidclOLD  16671  1stcrestlem  19174  hauspwdom  19223  ufilen  19621  dvle  21597  uhgrav  23373  umgraf2  23388  umgrares  23395  umisuhgra  23398  umgraun  23399  uslgrav  23406  usgrav  23407  uslgraf  23410  iscusgra0  23502  ntrivcvgn0  27549  isfne4  28681  refbas  28692  refssex  28693  fnetr  28698  reftr  28701  topfneec  28703  fnessref  28705  refssfne  28706  mapfien2OLD  29589  frisusgrapr  30723  linindsv  31088
  Copyright terms: Public domain W3C validator