Theorem brrelex2i 5689

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100  Rel wrel 5637

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639

This theorem is referenced by:  vtoclr  5695  brfvopabrbr  6946  domdifsn  9000  undom  9005  xpdom2  9012  xpdom1g  9014  domunsncan  9017  enfixsn  9026  fodomr  9068  pwdom  9069  domssex  9078  xpen  9080  mapdom1  9082  mapdom2  9088  pwen  9090  domtrfil  9128  sucdom2  9139  0sdom1dom  9158  1sdom2dom  9166  unxpdom  9171  unxpdom2  9172  sucxpdom  9173  isfinite2  9210  infn0ALT  9215  fin2inf  9216  fodomfir  9240  suppeqfsuppbi  9294  fsuppsssupp  9296  fsuppssov1  9299  fsuppunbi  9304  funsnfsupp  9307  mapfien2  9324  wemapso2  9470  card2on  9471  elharval  9478  harword  9480  brwdomi  9485  brwdomn0  9486  domwdom  9491  wdomtr  9492  wdompwdom  9495  canthwdom  9496  brwdom3i  9500  unwdomg  9501  xpwdomg  9502  unxpwdom  9506  infdifsn  9578  infdiffi  9579  isnum2  9869  wdomfil  9983  djuen  10092  djuenun  10093  djudom2  10106  djuxpdom  10108  djuinf  10111  infdju1  10112  pwdjuidm  10114  djulepw  10115  infdjuabs  10127  infdif  10130  pwdjudom  10137  infpss  10138  infmap2  10139  fictb  10166  infpssALT  10235  enfin2i  10243  fin34  10312  fodomb  10448  wdomac  10449  iundom2g  10462  iundom  10464  sdomsdomcard  10482  infxpidm  10484  engch  10551  fpwwe2lem3  10556  canthp1lem1  10575  canthp1lem2  10576  canthp1  10577  pwfseq  10587  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  hargch  10596  gchaclem  10601  hasheni  14283  hashdomi  14315  clim  15429  rlim  15430  ntrivcvgn0  15833  ssc1  17757  ssc2  17758  ssctr  17761  frgpnabl  19819  dprddomprc  19946  dprdval  19949  dprdgrp  19951  dprdf  19952  dprdssv  19962  subgdmdprd  19980  dprd2da  19988  1stcrestlem  23411  hauspwdom  23460  isref  23468  ufilen  23889  dvle  25983  ellpi  33470  finextfldext  33846  locfinref  34023  isfne4  36560  fnetr  36571  topfneec  36575  fnessref  36577  refssfne  36578  bj-epelb  37321  bj-idreseq  37421  phpreu  37859  sdomne0  43773  sdomne0d  43774  rn1st  45635  climf  45986  climf2  46028  iinfssc  49420  fuco21  49699  fucoid  49711