Theorem brrelex1i 5678

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 5675	. 2 ⊢ ((Rel 𝑅 ∧ 𝐴𝑅𝐵) → 𝐴 ∈ V)
3	1, 2	mpan 690	1 ⊢ (𝐴𝑅𝐵 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438   class class class wbr 5096  Rel wrel 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629

This theorem is referenced by:  nprrel  5681  opeliunxp2  5785  ideqg  5798  issetid  5801  dffv2  6927  brfvopabrbr  6936  brrpssg  7668  opeliunxp2f  8150  brtpos2  8172  brdomg  8893  ctex  8898  isfi  8910  domssr  8934  domdifsn  8986  xpdom2  8998  xpdom1g  9000  sbth  9023  sdomirr  9040  sdomdif  9051  fodomr  9054  pwdom  9055  xpen  9066  pwen  9076  sbthfi  9121  sucdom2  9125  fineqv  9165  infsdomnn  9199  relprcnfsupp  9265  fsuppssov1  9285  fsuppunbi  9290  mapfien2  9310  harword  9466  brwdom  9470  domwdom  9477  brwdom3i  9486  unwdomg  9487  xpwdomg  9488  infdifsn  9564  ac10ct  9942  inffien  9971  djuen  10078  djudom2  10092  djufi  10095  cdainflem  10096  djulepw  10101  infdjuabs  10113  infunabs  10114  infmap2  10125  cfslb2n  10176  fin4i  10206  isfin5  10207  isfin6  10208  fin4en1  10217  isfin4p1  10223  isfin32i  10273  fin45  10300  fin56  10301  fin67  10303  hsmexlem1  10334  hsmexlem3  10336  axcc3  10346  ttukeylem1  10417  brdom3  10436  iundom2g  10448  iundom  10450  gchi  10533  engch  10537  gchdomtri  10538  fpwwe2lem5  10544  fpwwe2lem6  10545  fpwwe2lem8  10547  gchdjuidm  10577  gchpwdom  10579  prcdnq  10902  reexALT  12895  hasheni  14269  hashdomi  14301  climcl  15420  climi  15431  climrlim2  15468  climrecl  15504  climge0  15505  iseralt  15606  climfsum  15741  structex  17075  issubc  17757  pmtrfv  19379  dprdval  19932  frgpcyg  21526  lindff  21768  lindfind  21769  f1lindf  21775  lindfmm  21780  lsslindf  21783  lbslcic  21794  psrbaglesupp  21876  hauspwdom  23443  refbas  23452  refssex  23453  reftr  23456  refun0  23457  ovoliunnul  25462  dvle  25966  cyclnspth  29823  hlimi  31212  gsumhashmul  33099  extdgval  33759  finextfldext  33770  usgrgt2cycl  35273  brsset  36030  brbigcup  36039  elfix2  36045  brcolinear2  36201  isfne  36482  refssfne  36501  bj-epelg  37212  bj-ideqb  37303  bj-opelidb1ALT  37310  ovoliunnfl  37802  voliunnfl  37804  volsupnfl  37805  brabg2  37857  heiborlem4  37954  isrngo  38037  isdivrngo  38090  brssr  38693  issetssr  38695  fphpd  43000  ctbnfien  43002  sdomne0  43596  climd  45858  climuzlem  45929  rlimdmafv  47365  rlimdmafv2  47446  imasubc  49338  imassc  49340  imaid  49341  imaf1co  49342  imasubc3  49343  fuco112  49516  fuco111  49517  fuco21  49523  fucoid  49535