Theorem brrelexi 5049

Description: The first argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by NM, 4-Jun-1998.)

Hypothesis

Ref	Expression
brrelexi.1	|- Rel R

Assertion

Ref	Expression
brrelexi	|- ( A R B -> A e. _V )

Proof of Theorem brrelexi

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 |- Rel R
2		brrelex 5047	. 2 |- ( ( Rel R /\ A R B ) -> A e. _V )
3	1, 2	mpan 670	1 |- ( A R B -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 1819   _Vcvv 3109   class class class wbr 4456   Rel wrel 5013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457  df-opab 4516  df-xp 5014  df-rel 5015

This theorem is referenced by:  nprrel  5051  vtoclr  5053  opeliunxp2  5151  ideqg  5164  issetid  5167  dffv2  5946  brrpssg  6581  brtpos2  6979  brdomg  7545  isfi  7558  en1uniel  7606  domdifsn  7619  undom  7624  xpdom2  7631  xpdom1g  7633  sbth  7656  dom0  7664  sdom0  7668  sdomirr  7673  sdomdif  7684  fodomr  7687  pwdom  7688  xpen  7699  pwen  7709  php3  7722  sucdom2  7733  sdom1  7738  fineqv  7754  f1finf1o  7765  infsdomnn  7799  relprcnfsupp  7850  fsuppimp  7853  fsuppunbi  7868  mapfien2  7886  harword  8009  brwdom  8011  domwdom  8018  brwdom3i  8027  unwdomg  8028  xpwdomg  8029  infdifsn  8090  ac10ct  8432  inffien  8461  iunfictbso  8512  cdaen  8570  cdadom1  8583  cdafi  8587  cdainflem  8588  cdalepw  8593  unctb  8602  infcdaabs  8603  infunabs  8604  infmap2  8615  cfslb2n  8665  fin4i  8695  isfin5  8696  isfin6  8697  fin4en1  8706  isfin4-3  8712  isfin32i  8762  fin45  8789  fin56  8790  fin67  8792  hsmexlem1  8823  hsmexlem3  8825  axcc3  8835  ttukeylem1  8906  brdom3  8923  iundom2g  8932  iundom  8934  iunctb  8966  gchi  9019  engch  9023  gchdomtri  9024  fpwwe2lem6  9030  fpwwe2lem7  9031  fpwwe2lem9  9033  gchpwdom  9065  prcdnq  9388  reexALT  11239  hasheni  12423  hashdomi  12450  brfi1uzind  12535  climcl  13333  climi  13344  climrlim2  13381  climrecl  13417  climge0  13418  iseralt  13518  climfsum  13645  strfv  14679  issubc  15250  pmtrfv  16603  dprdval  17160  dprdvalOLD  17162  cnfldex  18549  frgpcyg  18738  lindff  18976  lindfind  18977  f1lindf  18983  lindfmm  18988  lsslindf  18991  lbslcic  19002  eltopspOLD  19545  cctop  19633  1stcrestlem  20078  2ndcdisj2  20083  dis2ndc  20086  hauspwdom  20127  refbas  20136  refssex  20137  reftr  20140  refun0  20141  ovoliunnul  22043  uniiccdif  22112  dvle  22533  uhgrav  24422  ushgraf  24428  ushgrauhgra  24429  umgraf2  24443  umgrares  24450  umisuhgra  24453  uslgrav  24463  usgrav  24464  uslgraf  24471  iscusgra0  24583  eupap1  25102  eupath2lem3  25105  eupath2  25106  frisusgrapr  25117  isrngo  25506  isdivrngo  25559  hlimi  26231  brsset  29701  brbigcup  29710  elfix2  29716  brcolinear2  29870  ovoliunnfl  30218  voliunnfl  30220  volsupnfl  30221  isfne  30319  refssfne  30338  brabg2  30368  heiborlem4  30472  fphpd  30912  ctbnfien  30914  mapfien2OLD  31204  rlimdmafv  32423  linindsv  33148