Theorem brrelexi 4864

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

Syntax hints:   -> wi 4   e. wcel 1842   _Vcvv 3059   class class class wbr 4395   Rel wrel 4828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4517  ax-nul 4525  ax-pr 4630

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-br 4396  df-opab 4454  df-xp 4829  df-rel 4830

This theorem is referenced by:  nprrel  4866  vtoclr  4868  opeliunxp2  4962  ideqg  4975  issetid  4978  dffv2  5922  brrpssg  6564  brtpos2  6964  brdomg  7564  isfi  7577  en1uniel  7625  domdifsn  7638  undom  7643  xpdom2  7650  xpdom1g  7652  sbth  7675  dom0  7683  sdom0  7687  sdomirr  7692  sdomdif  7703  fodomr  7706  pwdom  7707  xpen  7718  pwen  7728  php3  7741  sucdom2  7751  sdom1  7755  fineqv  7770  f1finf1o  7781  infsdomnn  7815  relprcnfsupp  7866  fsuppimp  7869  fsuppunbi  7884  mapfien2  7902  harword  8025  brwdom  8027  domwdom  8034  brwdom3i  8043  unwdomg  8044  xpwdomg  8045  infdifsn  8106  ac10ct  8447  inffien  8476  iunfictbso  8527  cdaen  8585  cdadom1  8598  cdafi  8602  cdainflem  8603  cdalepw  8608  unctb  8617  infcdaabs  8618  infunabs  8619  infmap2  8630  cfslb2n  8680  fin4i  8710  isfin5  8711  isfin6  8712  fin4en1  8721  isfin4-3  8727  isfin32i  8777  fin45  8804  fin56  8805  fin67  8807  hsmexlem1  8838  hsmexlem3  8840  axcc3  8850  ttukeylem1  8921  brdom3  8938  iundom2g  8947  iundom  8949  iunctb  8981  gchi  9032  engch  9036  gchdomtri  9037  fpwwe2lem6  9043  fpwwe2lem7  9044  fpwwe2lem9  9046  gchpwdom  9078  prcdnq  9401  reexALT  11259  hasheni  12468  hashdomi  12496  brfi1uzind  12581  climcl  13471  climi  13482  climrlim2  13519  climrecl  13555  climge0  13556  iseralt  13656  climfsum  13785  strfv  14877  issubc  15448  pmtrfv  16801  dprdval  17354  dprdvalOLD  17356  cnfldex  18743  frgpcyg  18910  lindff  19142  lindfind  19143  f1lindf  19149  lindfmm  19154  lsslindf  19157  lbslcic  19168  eltopspOLD  19711  cctop  19799  1stcrestlem  20245  2ndcdisj2  20250  dis2ndc  20253  hauspwdom  20294  refbas  20303  refssex  20304  reftr  20307  refun0  20308  ovoliunnul  22210  uniiccdif  22279  dvle  22700  uhgrav  24713  ushgraf  24719  ushgrauhgra  24720  umgraf2  24734  umgrares  24741  umisuhgra  24744  uslgrav  24754  usgrav  24755  uslgraf  24762  iscusgra0  24874  eupap1  25393  eupath2lem3  25396  eupath2  25397  frisusgrapr  25408  isrngo  25794  isdivrngo  25847  hlimi  26519  brsset  30227  brbigcup  30236  elfix2  30242  brcolinear2  30396  isfne  30567  refssfne  30586  ovoliunnfl  31428  voliunnfl  31430  volsupnfl  31431  brabg2  31488  heiborlem4  31592  fphpd  35111  ctbnfien  35113  mapfien2OLD  35404  rlimdmafv  37630  linindsv  38557