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 674	1 |- ( A R B -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 1868   _Vcvv 3081   class class class wbr 4420   Rel wrel 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-xp 4856  df-rel 4857

This theorem is referenced by:  nprrel  4893  vtoclr  4895  opeliunxp2  4989  ideqg  5002  issetid  5005  dffv2  5951  brrpssg  6584  brtpos2  6984  brdomg  7584  isfi  7597  en1uniel  7645  domdifsn  7658  undom  7663  xpdom2  7670  xpdom1g  7672  sbth  7695  dom0  7703  sdom0  7707  sdomirr  7712  sdomdif  7723  fodomr  7726  pwdom  7727  xpen  7738  pwen  7748  php3  7761  sucdom2  7771  sdom1  7775  fineqv  7790  f1finf1o  7801  infsdomnn  7835  relprcnfsupp  7889  fsuppimp  7892  fsuppunbi  7907  mapfien2  7925  harword  8083  brwdom  8085  domwdom  8092  brwdom3i  8101  unwdomg  8102  xpwdomg  8103  infdifsn  8164  ac10ct  8466  inffien  8495  iunfictbso  8546  cdaen  8604  cdadom1  8617  cdafi  8621  cdainflem  8622  cdalepw  8627  unctb  8636  infcdaabs  8637  infunabs  8638  infmap2  8649  cfslb2n  8699  fin4i  8729  isfin5  8730  isfin6  8731  fin4en1  8740  isfin4-3  8746  isfin32i  8796  fin45  8823  fin56  8824  fin67  8826  hsmexlem1  8857  hsmexlem3  8859  axcc3  8869  ttukeylem1  8940  brdom3  8957  iundom2g  8966  iundom  8968  iunctb  9000  gchi  9050  engch  9054  gchdomtri  9055  fpwwe2lem6  9061  fpwwe2lem7  9062  fpwwe2lem9  9064  gchpwdom  9096  prcdnq  9419  reexALT  11297  hasheni  12531  hashdomi  12559  brfi1uzind  12647  climcl  13551  climi  13562  climrlim2  13599  climrecl  13635  climge0  13636  iseralt  13739  climfsum  13868  strfv  15145  issubc  15728  pmtrfv  17081  dprdval  17623  cnfldex  18961  frgpcyg  19131  lindff  19360  lindfind  19361  f1lindf  19367  lindfmm  19372  lsslindf  19375  lbslcic  19386  cctop  20008  1stcrestlem  20454  2ndcdisj2  20459  dis2ndc  20462  hauspwdom  20503  refbas  20512  refssex  20513  reftr  20516  refun0  20517  ovoliunnul  22447  uniiccdif  22522  dvle  22946  uhgrav  25010  ushgraf  25016  ushgrauhgra  25017  umgraf2  25031  umgrares  25038  umisuhgra  25041  uslgrav  25051  usgrav  25052  uslgraf  25059  iscusgra0  25171  eupap1  25690  eupath2lem3  25693  eupath2  25694  frisusgrapr  25705  isrngo  26092  isdivrngo  26145  hlimi  26827  brsset  30649  brbigcup  30658  elfix2  30664  brcolinear2  30818  isfne  30988  refssfne  31007  ovoliunnfl  31896  voliunnfl  31898  volsupnfl  31899  brabg2  31956  heiborlem4  32060  fphpd  35578  ctbnfien  35580  rlimdmafv  38391  linindsv  39512