Theorem brrelex1i 5710

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
brrelex1i	⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Proof of Theorem brrelex1i

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex1 5707	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   class class class wbr 5119  Rel wrel 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  nprrel  5713  opeliunxp2  5818  ideqg  5831  issetid  5834  dffv2  6973  brfvopabrbr  6982  brrpssg  7717  opeliunxp2f  8207  brtpos2  8229  brdomg  8969  brdomgOLD  8970  ctex  8976  isfi  8988  domssr  9011  domdifsn  9066  undomOLD  9072  xpdom2  9079  xpdom1g  9081  sucdom2OLD  9094  sbth  9105  dom0OLD  9115  sdom0OLD  9121  sdomirr  9126  sdomdif  9137  fodomr  9140  pwdom  9141  xpen  9152  pwen  9162  sbthfi  9211  sucdom2  9215  php3OLD  9231  sdom1OLD  9249  fineqv  9269  f1finf1oOLD  9276  infsdomnn  9308  infsdomnnOLD  9309  relprcnfsupp  9374  fsuppssov1  9394  fsuppunbi  9399  mapfien2  9419  harword  9575  brwdom  9579  domwdom  9586  brwdom3i  9595  unwdomg  9596  xpwdomg  9597  infdifsn  9669  ac10ct  10046  inffien  10075  djuen  10182  djudom2  10196  djufi  10199  cdainflem  10200  djulepw  10205  infdjuabs  10217  infunabs  10218  infmap2  10229  cfslb2n  10280  fin4i  10310  isfin5  10311  isfin6  10312  fin4en1  10321  isfin4p1  10327  isfin32i  10377  fin45  10404  fin56  10405  fin67  10407  hsmexlem1  10438  hsmexlem3  10440  axcc3  10450  ttukeylem1  10521  brdom3  10540  iundom2g  10552  iundom  10554  gchi  10636  engch  10640  gchdomtri  10641  fpwwe2lem5  10647  fpwwe2lem6  10648  fpwwe2lem8  10650  gchdjuidm  10680  gchpwdom  10682  prcdnq  11005  reexALT  12998  hasheni  14364  hashdomi  14396  climcl  15513  climi  15524  climrlim2  15561  climrecl  15597  climge0  15598  iseralt  15699  climfsum  15834  structex  17167  issubc  17846  pmtrfv  19431  dprdval  19984  frgpcyg  21532  lindff  21773  lindfind  21774  f1lindf  21780  lindfmm  21785  lsslindf  21788  lbslcic  21799  psrbaglesupp  21880  hauspwdom  23437  refbas  23446  refssex  23447  reftr  23450  refun0  23451  ovoliunnul  25458  dvle  25962  cyclnspth  29729  hlimi  31115  gsumhashmul  33001  extdgval  33641  usgrgt2cycl  35098  brsset  35853  brbigcup  35862  elfix2  35868  brcolinear2  36022  isfne  36303  refssfne  36322  bj-epelg  37032  bj-ideqb  37123  bj-opelidb1ALT  37130  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  brabg2  37687  heiborlem4  37784  isrngo  37867  isdivrngo  37920  brssr  38465  issetssr  38467  fphpd  42786  ctbnfien  42788  sdomne0  43384  climd  45649  climuzlem  45720  rlimdmafv  47154  rlimdmafv2  47235  imasubc  49039  imassc  49041  imaid  49042  imaf1co  49043  imasubc3  49044  fuco112  49188  fuco111  49189  fuco21  49195  fucoid  49207