Theorem brrelex1i 5687

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   class class class wbr 5085  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  nprrel  5690  opeliunxp2  5793  ideqg  5806  issetid  5809  dffv2  6935  brfvopabrbr  6944  brrpssg  7679  opeliunxp2f  8160  brtpos2  8182  brdomg  8905  ctex  8910  isfi  8922  domssr  8946  domdifsn  8998  xpdom2  9010  xpdom1g  9012  sbth  9035  sdomirr  9052  sdomdif  9063  fodomr  9066  pwdom  9067  xpen  9078  pwen  9088  sbthfi  9133  sucdom2  9137  fineqv  9177  infsdomnn  9211  relprcnfsupp  9277  fsuppssov1  9297  fsuppunbi  9302  mapfien2  9322  harword  9478  brwdom  9482  domwdom  9489  brwdom3i  9498  unwdomg  9499  xpwdomg  9500  infdifsn  9578  ac10ct  9956  inffien  9985  djuen  10092  djudom2  10106  djufi  10109  cdainflem  10110  djulepw  10115  infdjuabs  10127  infunabs  10128  infmap2  10139  cfslb2n  10190  fin4i  10220  isfin5  10221  isfin6  10222  fin4en1  10231  isfin4p1  10237  isfin32i  10287  fin45  10314  fin56  10315  fin67  10317  hsmexlem1  10348  hsmexlem3  10350  axcc3  10360  ttukeylem1  10431  brdom3  10450  iundom2g  10462  iundom  10464  gchi  10547  engch  10551  gchdomtri  10552  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  gchdjuidm  10591  gchpwdom  10593  prcdnq  10916  reexALT  12934  hasheni  14310  hashdomi  14342  climcl  15461  climi  15472  climrlim2  15509  climrecl  15545  climge0  15546  iseralt  15647  climfsum  15783  structex  17120  issubc  17802  pmtrfv  19427  dprdval  19980  frgpcyg  21553  lindff  21795  lindfind  21796  f1lindf  21802  lindfmm  21807  lsslindf  21810  lbslcic  21821  psrbaglesupp  21902  hauspwdom  23466  refbas  23475  refssex  23476  reftr  23479  refun0  23480  ovoliunnul  25474  dvle  25974  cyclnspth  29869  hlimi  31259  gsumhashmul  33128  extdgval  33797  finextfldext  33808  usgrgt2cycl  35312  brsset  36069  brbigcup  36078  elfix2  36084  brcolinear2  36240  isfne  36521  refssfne  36540  bj-epelg  37375  bj-ideqb  37473  bj-opelidb1ALT  37480  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  brabg2  38038  heiborlem4  38135  isrngo  38218  isdivrngo  38271  brssr  38902  issetssr  38904  fphpd  43244  ctbnfien  43246  sdomne0  43840  climd  46100  climuzlem  46171  rlimdmafv  47625  rlimdmafv2  47706  imasubc  49626  imassc  49628  imaid  49629  imaf1co  49630  imasubc3  49631  fuco112  49804  fuco111  49805  fuco21  49811  fucoid  49823