Theorem brrelexi 4875

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 4873	. 2 |- ( ( Rel R /\ A R B ) -> A e. _V )
3	1, 2	mpan 665	1 |- ( A R B -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 1761   _Vcvv 2970   class class class wbr 4289   Rel wrel 4841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-xp 4842  df-rel 4843

This theorem is referenced by:  nprrel  4877  vtoclr  4879  opeliunxp2  4974  ideqg  4987  issetid  4990  dffv2  5761  brrpssg  6361  brtpos2  6750  brdomg  7316  isfi  7329  en1uniel  7377  domdifsn  7390  undom  7395  xpdom2  7402  xpdom1g  7404  sbth  7427  dom0  7435  sdom0  7439  sdomirr  7444  sdomdif  7455  fodomr  7458  pwdom  7459  xpen  7470  pwen  7480  php3  7493  sucdom2  7503  sdom1  7508  fineqv  7524  f1finf1o  7535  infsdomnn  7569  relprcnfsupp  7619  fsuppimp  7622  fsuppunbi  7637  mapfien2  7654  harword  7776  brwdom  7778  domwdom  7785  brwdom3i  7794  unwdomg  7795  xpwdomg  7796  infdifsn  7858  ac10ct  8200  inffien  8229  iunfictbso  8280  cdaen  8338  cdadom1  8351  cdafi  8355  cdainflem  8356  cdalepw  8361  unctb  8370  infcdaabs  8371  infunabs  8372  infmap2  8383  cfslb2n  8433  fin4i  8463  isfin5  8464  isfin6  8465  fin4en1  8474  isfin4-3  8480  isfin32i  8530  fin45  8557  fin56  8558  fin67  8560  hsmexlem1  8591  hsmexlem3  8593  axcc3  8603  ttukeylem1  8674  brdom3  8691  iundom2g  8700  iundom  8702  iunctb  8734  gchi  8787  engch  8791  gchdomtri  8792  fpwwe2lem6  8798  fpwwe2lem7  8799  fpwwe2lem9  8801  gchpwdom  8833  prcdnq  9158  reexALT  10981  hasheni  12115  hashdomi  12139  brfi1uzind  12215  climcl  12973  climi  12984  climrlim2  13021  climrecl  13057  climge0  13058  iseralt  13158  climfsum  13279  strfv  14204  issubc  14744  pmtrfv  15951  dprdval  16475  dprdvalOLD  16477  cnfldex  17721  frgpcyg  17906  lindff  18144  lindfind  18145  f1lindf  18151  lindfmm  18156  lsslindf  18159  lbslcic  18170  eltopspOLD  18423  cctop  18510  1stcrestlem  18956  2ndcdisj2  18961  dis2ndc  18964  hauspwdom  19005  ovoliunnul  20890  uniiccdif  20958  dvle  21379  uhgrav  23155  umgraf2  23170  umgrares  23177  umisuhgra  23180  uslgrav  23188  usgrav  23189  uslgraf  23192  iscusgra0  23284  eupap1  23516  eupath2lem3  23519  eupath2  23520  isrngo  23784  isdivrngo  23837  hlimi  24509  brsset  27833  brbigcup  27842  elfix2  27848  brcolinear2  28002  ovoliunnfl  28342  voliunnfl  28344  volsupnfl  28345  isfne  28449  isref  28460  refssfne  28475  brabg2  28518  heiborlem4  28622  fphpd  29064  ctbnfien  29066  mapfien2OLD  29358  rlimdmafv  29992  frisusgrapr  30492  linindsv  30803