Theorem brrelex2i 5591

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

Syntax hints:   → wi 4   ∈ wcel 2112  Vcvv 3398   class class class wbr 5039  Rel wrel 5541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-rel 5543

This theorem is referenced by:  vtoclr  5597  brfvopabrbr  6793  brdomi  8617  domdifsn  8706  undom  8711  xpdom2  8718  xpdom1g  8720  domunsncan  8723  enfixsn  8732  sucdom2  8733  fodomr  8775  pwdom  8776  domssex  8785  xpen  8787  mapdom1  8789  mapdom2  8795  pwen  8797  unxpdom  8861  unxpdom2  8862  sucxpdom  8863  isfinite2  8907  infn0  8911  fin2inf  8912  suppeqfsuppbi  8977  fsuppsssupp  8979  fsuppunbi  8984  funsnfsupp  8987  mapfien2  9003  wemapso2  9147  card2on  9148  elharval  9155  harword  9157  brwdomi  9162  brwdomn0  9163  domwdom  9168  wdomtr  9169  wdompwdom  9172  canthwdom  9173  brwdom3i  9177  unwdomg  9178  xpwdomg  9179  unxpwdom  9183  infdifsn  9250  infdiffi  9251  isnum2  9526  wdomfil  9640  djuen  9748  djuenun  9749  djudom2  9762  djuxpdom  9764  djuinf  9767  infdju1  9768  pwdjuidm  9770  djulepw  9771  infdjuabs  9785  infdif  9788  pwdjudom  9795  infpss  9796  infmap2  9797  fictb  9824  infpssALT  9892  enfin2i  9900  fin34  9969  fodomb  10105  wdomac  10106  iundom2g  10119  iundom  10121  sdomsdomcard  10139  infxpidm  10141  engch  10207  fpwwe2lem3  10212  canthp1lem1  10231  canthp1lem2  10232  canthp1  10233  pwfseq  10243  pwxpndom2  10244  pwxpndom  10245  pwdjundom  10246  hargch  10252  gchaclem  10257  hasheni  13879  hashdomi  13912  clim  15020  rlim  15021  ntrivcvgn0  15425  ssc1  17280  ssc2  17281  ssctr  17284  frgpnabl  19214  dprddomprc  19341  dprdval  19344  dprdgrp  19346  dprdf  19347  dprdssv  19357  subgdmdprd  19375  dprd2da  19383  1stcrestlem  22303  hauspwdom  22352  isref  22360  ufilen  22781  dvle  24858  locfinref  31459  isfne4  34215  fnetr  34226  topfneec  34230  fnessref  34232  refssfne  34233  bj-epelb  34925  bj-idreseq  35017  phpreu  35447  climf  42781  climf2  42825