Theorem brrelexi 5039

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 5037	. 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 1767   _Vcvv 3113   class class class wbr 4447   Rel wrel 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-rel 5006

This theorem is referenced by:  nprrel  5041  vtoclr  5043  opeliunxp2  5140  ideqg  5153  issetid  5156  dffv2  5939  brrpssg  6565  brtpos2  6961  brdomg  7526  isfi  7539  en1uniel  7587  domdifsn  7600  undom  7605  xpdom2  7612  xpdom1g  7614  sbth  7637  dom0  7645  sdom0  7649  sdomirr  7654  sdomdif  7665  fodomr  7668  pwdom  7669  xpen  7680  pwen  7690  php3  7703  sucdom2  7714  sdom1  7719  fineqv  7735  f1finf1o  7746  infsdomnn  7780  relprcnfsupp  7831  fsuppimp  7834  fsuppunbi  7849  mapfien2  7867  harword  7990  brwdom  7992  domwdom  7999  brwdom3i  8008  unwdomg  8009  xpwdomg  8010  infdifsn  8072  ac10ct  8414  inffien  8443  iunfictbso  8494  cdaen  8552  cdadom1  8565  cdafi  8569  cdainflem  8570  cdalepw  8575  unctb  8584  infcdaabs  8585  infunabs  8586  infmap2  8597  cfslb2n  8647  fin4i  8677  isfin5  8678  isfin6  8679  fin4en1  8688  isfin4-3  8694  isfin32i  8744  fin45  8771  fin56  8772  fin67  8774  hsmexlem1  8805  hsmexlem3  8807  axcc3  8817  ttukeylem1  8888  brdom3  8905  iundom2g  8914  iundom  8916  iunctb  8948  gchi  9001  engch  9005  gchdomtri  9006  fpwwe2lem6  9012  fpwwe2lem7  9013  fpwwe2lem9  9015  gchpwdom  9047  prcdnq  9370  reexALT  11213  hasheni  12388  hashdomi  12415  brfi1uzind  12497  climcl  13284  climi  13295  climrlim2  13332  climrecl  13368  climge0  13369  iseralt  13469  climfsum  13596  strfv  14523  issubc  15064  pmtrfv  16280  dprdval  16834  dprdvalOLD  16836  cnfldex  18210  frgpcyg  18395  lindff  18633  lindfind  18634  f1lindf  18640  lindfmm  18645  lsslindf  18648  lbslcic  18659  eltopspOLD  19202  cctop  19289  1stcrestlem  19735  2ndcdisj2  19740  dis2ndc  19743  hauspwdom  19784  ovoliunnul  21669  uniiccdif  21738  dvle  22159  uhgrav  23988  ushgraf  23994  ushgrauhgra  23995  umgraf2  24009  umgrares  24016  umisuhgra  24019  uslgrav  24029  usgrav  24030  uslgraf  24037  iscusgra0  24149  eupap1  24668  eupath2lem3  24671  eupath2  24672  frisusgrapr  24683  isrngo  25072  isdivrngo  25125  hlimi  25797  brsset  29132  brbigcup  29141  elfix2  29147  brcolinear2  29301  ovoliunnfl  29649  voliunnfl  29651  volsupnfl  29652  isfne  29756  isref  29767  refssfne  29782  brabg2  29825  heiborlem4  29929  fphpd  30370  ctbnfien  30372  mapfien2OLD  30662  rlimdmafv  31745  linindsv  32136