Theorem brrelex2i 5683

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   class class class wbr 5086  Rel wrel 5631

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 5232  ax-pr 5372

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5632  df-rel 5633

This theorem is referenced by:  vtoclr  5689  brfvopabrbr  6940  domdifsn  8993  undom  8998  xpdom2  9005  xpdom1g  9007  domunsncan  9010  enfixsn  9019  fodomr  9061  pwdom  9062  domssex  9071  xpen  9073  mapdom1  9075  mapdom2  9081  pwen  9083  domtrfil  9121  sucdom2  9132  0sdom1dom  9151  1sdom2dom  9159  unxpdom  9164  unxpdom2  9165  sucxpdom  9166  isfinite2  9203  infn0ALT  9208  fin2inf  9209  fodomfir  9233  suppeqfsuppbi  9287  fsuppsssupp  9289  fsuppssov1  9292  fsuppunbi  9297  funsnfsupp  9300  mapfien2  9317  wemapso2  9463  card2on  9464  elharval  9471  harword  9473  brwdomi  9478  brwdomn0  9479  domwdom  9484  wdomtr  9485  wdompwdom  9488  canthwdom  9489  brwdom3i  9493  unwdomg  9494  xpwdomg  9495  unxpwdom  9499  infdifsn  9573  infdiffi  9574  isnum2  9864  wdomfil  9978  djuen  10087  djuenun  10088  djudom2  10101  djuxpdom  10103  djuinf  10106  infdju1  10107  pwdjuidm  10109  djulepw  10110  infdjuabs  10122  infdif  10125  pwdjudom  10132  infpss  10133  infmap2  10134  fictb  10161  infpssALT  10230  enfin2i  10238  fin34  10307  fodomb  10443  wdomac  10444  iundom2g  10457  iundom  10459  sdomsdomcard  10477  infxpidm  10479  engch  10546  fpwwe2lem3  10551  canthp1lem1  10570  canthp1lem2  10571  canthp1  10572  pwfseq  10582  pwxpndom2  10583  pwxpndom  10584  pwdjundom  10585  hargch  10591  gchaclem  10596  hasheni  14305  hashdomi  14337  clim  15451  rlim  15452  ntrivcvgn0  15858  ssc1  17783  ssc2  17784  ssctr  17787  frgpnabl  19845  dprddomprc  19972  dprdval  19975  dprdgrp  19977  dprdf  19978  dprdssv  19988  subgdmdprd  20006  dprd2da  20014  1stcrestlem  23431  hauspwdom  23480  isref  23488  ufilen  23909  dvle  25988  ellpi  33452  finextfldext  33828  locfinref  34005  isfne4  36542  fnetr  36553  topfneec  36557  fnessref  36559  refssfne  36560  bj-epelb  37396  bj-idreseq  37496  phpreu  37943  sdomne0  43862  sdomne0d  43863  rn1st  45724  climf  46074  climf2  46116  iinfssc  49548  fuco21  49827  fucoid  49839