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

Theorem brrelex2i 4911
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 4909 . 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 2948   class class class wbr 4204   Rel wrel 4875
This theorem is referenced by:  vtoclr  4914  brdomi  7111  domdifsn  7183  undom  7188  xpdom2  7195  xpdom1g  7197  domunsncan  7200  fodomr  7250  pwdom  7251  domssex  7260  xpen  7262  mapdom1  7264  mapdom2  7270  pwen  7272  sucdom2  7295  unxpdom  7308  unxpdom2  7309  sucxpdom  7310  isfinite2  7357  infn0  7361  fin2inf  7362  card2on  7514  elharval  7523  harword  7525  brwdomi  7528  brwdomn0  7529  domwdom  7534  wdomtr  7535  wdompwdom  7538  canthwdom  7539  brwdom3i  7543  unwdomg  7544  xpwdomg  7545  unxpwdom  7549  infdifsn  7603  infdiffi  7604  isnum2  7824  wdomfil  7934  cdaen  8045  cdaenun  8046  cdadom1  8058  cdaxpdom  8061  cdainf  8064  infcda1  8065  pwcdaidm  8067  cdalepw  8068  infpss  8089  infmap2  8090  fictb  8117  infpssALT  8185  enfin2i  8193  fin34  8262  fodomb  8396  wdomac  8397  iundom2g  8407  iundom  8409  sdomsdomcard  8427  infxpidm  8429  engch  8495  fpwwe2lem3  8500  canthp1lem1  8519  canthp1lem2  8520  canthp1  8521  pwfseq  8531  pwxpndom2  8532  pwxpndom  8533  pwcdandom  8534  gchaclem  8537  hargch  8544  hasheni  11624  hashdomi  11646  brfi1uzind  11707  clim  12280  rlim  12281  ssc1  14013  ssc2  14014  ssctr  14017  frgpnabl  15478  dprdval  15553  dprdgrp  15555  dprdf  15556  dprdcntz  15558  dprddisj  15559  dprdw  15560  dprdssv  15566  dprdfid  15567  dprdfinv  15569  dprdfadd  15570  dprdfsub  15571  dprdfeq0  15572  dprdf11  15573  dprdlub  15576  dprdres  15578  dprdss  15579  dprdf1o  15582  subgdmdprd  15584  dmdprdsplitlem  15587  dprddisj2  15589  dprd2da  15592  dmdprdsplit2  15596  dpjfval  15605  dpjidcl  15608  1stcrestlem  17507  hauspwdom  17556  ufilen  17954  dvle  19883  uhgrav  21329  umgraf2  21344  umgrares  21351  umisuhgra  21354  umgraun  21355  uslgrav  21362  usgrav  21363  uslgraf  21366  iscusgra0  21458  ntrivcvgn0  25218  isfne4  26340  refbas  26351  refssex  26352  fnetr  26357  reftr  26360  topfneec  26362  fnessref  26364  refssfne  26365  enfixsn  27225  mapfien2  27226  frisusgrapr  28318
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 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-xp 4876  df-rel 4877
  Copyright terms: Public domain W3C validator