Theorem brrelexi 4894

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

Syntax hints:   -> wi 4   e. wcel 1898   _Vcvv 3057   class class class wbr 4416   Rel wrel 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-xp 4859  df-rel 4860

This theorem is referenced by:  nprrel  4896  vtoclr  4898  opeliunxp2  4992  ideqg  5005  issetid  5008  dffv2  5961  brrpssg  6600  opeliunxp2f  6983  brtpos2  7005  brdomg  7605  isfi  7619  en1uniel  7667  domdifsn  7681  undom  7686  xpdom2  7693  xpdom1g  7695  sbth  7718  dom0  7726  sdom0  7730  sdomirr  7735  sdomdif  7746  fodomr  7749  pwdom  7750  xpen  7761  pwen  7771  php3  7784  sucdom2  7794  sdom1  7798  fineqv  7813  f1finf1o  7824  infsdomnn  7858  relprcnfsupp  7912  fsuppimp  7915  fsuppunbi  7930  mapfien2  7948  harword  8106  brwdom  8108  domwdom  8115  brwdom3i  8124  unwdomg  8125  xpwdomg  8126  infdifsn  8188  ac10ct  8491  inffien  8520  iunfictbso  8571  cdaen  8629  cdadom1  8642  cdafi  8646  cdainflem  8647  cdalepw  8652  unctb  8661  infcdaabs  8662  infunabs  8663  infmap2  8674  cfslb2n  8724  fin4i  8754  isfin5  8755  isfin6  8756  fin4en1  8765  isfin4-3  8771  isfin32i  8821  fin45  8848  fin56  8849  fin67  8851  hsmexlem1  8882  hsmexlem3  8884  axcc3  8894  ttukeylem1  8965  brdom3  8982  iundom2g  8991  iundom  8993  iunctb  9025  gchi  9075  engch  9079  gchdomtri  9080  fpwwe2lem6  9086  fpwwe2lem7  9087  fpwwe2lem9  9089  gchpwdom  9121  prcdnq  9444  reexALT  11325  hasheni  12563  hashdomi  12591  brfi1indALT  12686  climcl  13612  climi  13623  climrlim2  13660  climrecl  13696  climge0  13697  iseralt  13800  climfsum  13929  strfv  15206  issubc  15789  pmtrfv  17142  dprdval  17684  cnfldex  19022  frgpcyg  19193  lindff  19422  lindfind  19423  f1lindf  19429  lindfmm  19434  lsslindf  19437  lbslcic  19448  cctop  20070  1stcrestlem  20516  2ndcdisj2  20521  dis2ndc  20524  hauspwdom  20565  refbas  20574  refssex  20575  reftr  20578  refun0  20579  ovoliunnul  22509  uniiccdif  22584  dvle  23008  uhgrav  25072  ushgraf  25078  ushgrauhgra  25079  umgraf2  25093  umgrares  25100  umisuhgra  25103  uslgrav  25113  usgrav  25114  uslgraf  25121  iscusgra0  25234  eupap1  25753  eupath2lem3  25756  eupath2  25757  frisusgrapr  25768  isrngo  26155  isdivrngo  26208  hlimi  26890  brsset  30705  brbigcup  30714  elfix2  30720  brcolinear2  30874  isfne  31044  refssfne  31063  ovoliunnfl  32027  voliunnfl  32029  volsupnfl  32030  brabg2  32087  heiborlem4  32191  fphpd  35704  ctbnfien  35706  rlimdmafv  38717  subgrv  39392  linindsv  40511