Theorem brrelex2i 5679

Description: The second argument of a binary relation exists. (An artifact of our ordered pair definition.) (Contributed by Mario Carneiro, 26-Apr-2015.)

Hypothesis

Ref	Expression
brrelexi.1	⊢ Rel 𝑅

Assertion

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

Proof of Theorem brrelex2i

Step	Hyp	Ref	Expression
1		brrelexi.1	. 2 ⊢ Rel 𝑅
2		brrelex2 5676	. 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:  vtoclr  5685  brfvopabrbr  6936  domdifsn  8986  undom  8991  xpdom2  8998  xpdom1g  9000  domunsncan  9003  enfixsn  9012  fodomr  9054  pwdom  9055  domssex  9064  xpen  9066  mapdom1  9068  mapdom2  9074  pwen  9076  domtrfil  9114  sucdom2  9125  0sdom1dom  9144  1sdom2dom  9152  unxpdom  9157  unxpdom2  9158  sucxpdom  9159  isfinite2  9196  infn0ALT  9201  fin2inf  9202  fodomfir  9226  suppeqfsuppbi  9280  fsuppsssupp  9282  fsuppssov1  9285  fsuppunbi  9290  funsnfsupp  9293  mapfien2  9310  wemapso2  9456  card2on  9457  elharval  9464  harword  9466  brwdomi  9471  brwdomn0  9472  domwdom  9477  wdomtr  9478  wdompwdom  9481  canthwdom  9482  brwdom3i  9486  unwdomg  9487  xpwdomg  9488  unxpwdom  9492  infdifsn  9564  infdiffi  9565  isnum2  9855  wdomfil  9969  djuen  10078  djuenun  10079  djudom2  10092  djuxpdom  10094  djuinf  10097  infdju1  10098  pwdjuidm  10100  djulepw  10101  infdjuabs  10113  infdif  10116  pwdjudom  10123  infpss  10124  infmap2  10125  fictb  10152  infpssALT  10221  enfin2i  10229  fin34  10298  fodomb  10434  wdomac  10435  iundom2g  10448  iundom  10450  sdomsdomcard  10468  infxpidm  10470  engch  10537  fpwwe2lem3  10542  canthp1lem1  10561  canthp1lem2  10562  canthp1  10563  pwfseq  10573  pwxpndom2  10574  pwxpndom  10575  pwdjundom  10576  hargch  10582  gchaclem  10587  hasheni  14269  hashdomi  14301  clim  15415  rlim  15416  ntrivcvgn0  15819  ssc1  17743  ssc2  17744  ssctr  17747  frgpnabl  19802  dprddomprc  19929  dprdval  19932  dprdgrp  19934  dprdf  19935  dprdssv  19945  subgdmdprd  19963  dprd2da  19971  1stcrestlem  23394  hauspwdom  23443  isref  23451  ufilen  23872  dvle  25966  ellpi  33403  finextfldext  33770  locfinref  33947  isfne4  36483  fnetr  36494  topfneec  36498  fnessref  36500  refssfne  36501  bj-epelb  37213  bj-idreseq  37306  phpreu  37744  sdomne0  43596  sdomne0d  43597  rn1st  45459  climf  45810  climf2  45852  iinfssc  49244  fuco21  49523  fucoid  49535