Theorem brrelex2i 5719

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463   class class class wbr 5113  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-rel 5669

This theorem is referenced by:  vtoclr  5725  brfvopabrbr  6987  domdifsn  9048  undom  9053  xpdom2  9060  xpdom1g  9062  domunsncan  9065  enfixsn  9074  fodomr  9116  pwdom  9117  domssex  9126  xpen  9128  mapdom1  9130  mapdom2  9136  pwen  9138  domtrfil  9176  sucdom2  9187  0sdom1dom  9206  1sdom2dom  9214  unxpdom  9219  unxpdom2  9220  sucxpdom  9221  isfinite2  9258  infn0ALT  9263  fin2inf  9264  fodomfir  9287  suppeqfsuppbi  9339  fsuppsssupp  9341  fsuppssov1  9344  fsuppunbi  9349  funsnfsupp  9352  mapfien2  9369  wemapso2  9515  card2on  9516  elharval  9523  harword  9525  brwdomi  9530  brwdomn0  9531  domwdom  9536  wdomtr  9537  wdompwdom  9540  canthwdom  9541  brwdom3i  9545  unwdomg  9546  xpwdomg  9547  unxpwdom  9551  infdifsn  9626  infdiffi  9627  isnum2  9931  wdomfil  10045  djuen  10153  djuenun  10154  djudom2  10167  djuxpdom  10169  djuinf  10172  infdju1  10173  pwdjuidm  10175  djulepw  10176  infdjuabs  10188  infdif  10191  pwdjudom  10198  infpss  10199  infmap2  10200  fictb  10227  infpssALT  10297  enfin2i  10305  fin34  10374  fodomb  10510  wdomac  10511  iundom2g  10524  iundom  10526  sdomsdomcard  10544  infxpidm  10546  engch  10613  fpwwe2lem3  10618  canthp1lem1  10637  canthp1lem2  10638  canthp1  10639  pwfseq  10649  pwxpndom2  10650  pwxpndom  10651  pwdjundom  10652  hargch  10658  gchaclem  10663  hasheni  14384  hashdomi  14416  clim  15545  rlim  15546  ntrivcvgn0  15952  ssc1  17878  ssc2  17879  ssctr  17882  frgpnabl  19945  dprddomprc  20072  dprdval  20075  dprdgrp  20077  dprdf  20078  dprdssv  20088  subgdmdprd  20106  dprd2da  20114  1stcrestlem  23578  hauspwdom  23627  isref  23635  ufilen  24056  dvle  26135  ellpi  33630  finextfldext  33999  locfinref  34176  karddom  35507  kardsdom  35508  isfne4  36774  fnetr  36785  topfneec  36789  fnessref  36791  refssfne  36792  bj-epelb  37627  bj-idreseq  37728  phpreu  38177  sdomne0  44065  sdomne0d  44066  rn1st  45914  climf  46264  climf2  46306  iinfssc  49754  fuco21  50033  fucoid  50045