Theorem brrelexi 4891

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 4889	. 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 1756   _Vcvv 2984   class class class wbr 4304   Rel wrel 4857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4425  ax-nul 4433  ax-pr 4543

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-ral 2732  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363  df-xp 4858  df-rel 4859

This theorem is referenced by:  nprrel  4893  vtoclr  4895  opeliunxp2  4990  ideqg  5003  issetid  5006  dffv2  5776  brrpssg  6374  brtpos2  6763  brdomg  7332  isfi  7345  en1uniel  7393  domdifsn  7406  undom  7411  xpdom2  7418  xpdom1g  7420  sbth  7443  dom0  7451  sdom0  7455  sdomirr  7460  sdomdif  7471  fodomr  7474  pwdom  7475  xpen  7486  pwen  7496  php3  7509  sucdom2  7519  sdom1  7524  fineqv  7540  f1finf1o  7551  infsdomnn  7585  relprcnfsupp  7635  fsuppimp  7638  fsuppunbi  7653  mapfien2  7670  harword  7792  brwdom  7794  domwdom  7801  brwdom3i  7810  unwdomg  7811  xpwdomg  7812  infdifsn  7874  ac10ct  8216  inffien  8245  iunfictbso  8296  cdaen  8354  cdadom1  8367  cdafi  8371  cdainflem  8372  cdalepw  8377  unctb  8386  infcdaabs  8387  infunabs  8388  infmap2  8399  cfslb2n  8449  fin4i  8479  isfin5  8480  isfin6  8481  fin4en1  8490  isfin4-3  8496  isfin32i  8546  fin45  8573  fin56  8574  fin67  8576  hsmexlem1  8607  hsmexlem3  8609  axcc3  8619  ttukeylem1  8690  brdom3  8707  iundom2g  8716  iundom  8718  iunctb  8750  gchi  8803  engch  8807  gchdomtri  8808  fpwwe2lem6  8814  fpwwe2lem7  8815  fpwwe2lem9  8817  gchpwdom  8849  prcdnq  9174  reexALT  10997  hasheni  12131  hashdomi  12155  brfi1uzind  12231  climcl  12989  climi  13000  climrlim2  13037  climrecl  13073  climge0  13074  iseralt  13174  climfsum  13295  strfv  14220  issubc  14760  pmtrfv  15970  dprdval  16497  dprdvalOLD  16499  cnfldex  17833  frgpcyg  18018  lindff  18256  lindfind  18257  f1lindf  18263  lindfmm  18268  lsslindf  18271  lbslcic  18282  eltopspOLD  18535  cctop  18622  1stcrestlem  19068  2ndcdisj2  19073  dis2ndc  19076  hauspwdom  19117  ovoliunnul  21002  uniiccdif  21070  dvle  21491  uhgrav  23248  umgraf2  23263  umgrares  23270  umisuhgra  23273  uslgrav  23281  usgrav  23282  uslgraf  23285  iscusgra0  23377  eupap1  23609  eupath2lem3  23612  eupath2  23613  isrngo  23877  isdivrngo  23930  hlimi  24602  brsset  27932  brbigcup  27941  elfix2  27947  brcolinear2  28101  ovoliunnfl  28445  voliunnfl  28447  volsupnfl  28448  isfne  28552  isref  28563  refssfne  28578  brabg2  28621  heiborlem4  28725  fphpd  29167  ctbnfien  29169  mapfien2OLD  29461  rlimdmafv  30095  frisusgrapr  30595  linindsv  30991