Theorem brrelexi 5082

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 𝑅

Assertion

Ref	Expression
brrelexi	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Proof of Theorem brrelexi

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex 5080	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 702	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173   class class class wbr 4583  Rel wrel 5043

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-rel 5045

This theorem is referenced by:  nprrel  5084  vtoclr  5086  opeliunxp2  5182  ideqg  5195  issetid  5198  dffv2  6181  brrpssg  6837  opeliunxp2f  7223  brtpos2  7245  brdomg  7851  isfi  7865  en1uniel  7914  domdifsn  7928  undom  7933  xpdom2  7940  xpdom1g  7942  sbth  7965  dom0  7973  sdom0  7977  sdomirr  7982  sdomdif  7993  fodomr  7996  pwdom  7997  xpen  8008  pwen  8018  php3  8031  sucdom2  8041  sdom1  8045  fineqv  8060  f1finf1o  8072  infsdomnn  8106  relprcnfsupp  8161  fsuppimp  8164  fsuppunbi  8179  mapfien2  8197  harword  8353  brwdom  8355  domwdom  8362  brwdom3i  8371  unwdomg  8372  xpwdomg  8373  infdifsn  8437  ac10ct  8740  inffien  8769  iunfictbso  8820  cdaen  8878  cdadom1  8891  cdafi  8895  cdainflem  8896  cdalepw  8901  unctb  8910  infcdaabs  8911  infunabs  8912  infmap2  8923  cfslb2n  8973  fin4i  9003  isfin5  9004  isfin6  9005  fin4en1  9014  isfin4-3  9020  isfin32i  9070  fin45  9097  fin56  9098  fin67  9100  hsmexlem1  9131  hsmexlem3  9133  axcc3  9143  ttukeylem1  9214  brdom3  9231  iundom2g  9241  iundom  9243  iunctb  9275  gchi  9325  engch  9329  gchdomtri  9330  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  gchpwdom  9371  prcdnq  9694  reexALT  11702  hasheni  12998  hashdomi  13030  brfi1indALT  13137  brfi1indALTOLD  13143  climcl  14078  climi  14089  climrlim2  14126  climrecl  14162  climge0  14163  iseralt  14263  climfsum  14393  strfv  15735  issubc  16318  pmtrfv  17695  dprdval  18225  cnfldex  19570  frgpcyg  19741  lindff  19973  lindfind  19974  f1lindf  19980  lindfmm  19985  lsslindf  19988  lbslcic  19999  1stcrestlem  21065  2ndcdisj2  21070  dis2ndc  21073  hauspwdom  21114  refbas  21123  refssex  21124  reftr  21127  refun0  21128  ovoliunnul  23082  uniiccdif  23152  dvle  23574  uhgrav  25825  ushgraf  25831  ushgrauhgra  25832  umgraf2  25846  umgrares  25853  umisuhgra  25856  uslgrav  25866  usgrav  25867  uslgraf  25874  iscusgra0  25986  eupap1  26503  eupath2lem3  26506  eupath2  26507  frisusgrapr  26518  hlimi  27429  brsset  31166  brbigcup  31175  elfix2  31181  brcolinear2  31335  isfne  31504  refssfne  31523  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  brabg2  32680  heiborlem4  32783  isrngo  32866  isdivrngo  32919  fphpd  36398  ctbnfien  36400  climd  38739  rlimdmafv  39906  subgrv  40494  linindsv  42028