Theorem brrelex2i 5688

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444   class class class wbr 5102  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  vtoclr  5694  brfvopabrbr  6947  domdifsn  9001  undom  9006  xpdom2  9013  xpdom1g  9015  domunsncan  9018  enfixsn  9027  fodomr  9069  pwdom  9070  domssex  9079  xpen  9081  mapdom1  9083  mapdom2  9089  pwen  9091  domtrfil  9133  sucdom2  9144  0sdom1dom  9162  1sdom2dom  9170  unxpdom  9176  unxpdom2  9177  sucxpdom  9178  isfinite2  9221  infn0ALT  9228  fin2inf  9229  fodomfir  9255  suppeqfsuppbi  9306  fsuppsssupp  9308  fsuppssov1  9311  fsuppunbi  9316  funsnfsupp  9319  mapfien2  9336  wemapso2  9482  card2on  9483  elharval  9490  harword  9492  brwdomi  9497  brwdomn0  9498  domwdom  9503  wdomtr  9504  wdompwdom  9507  canthwdom  9508  brwdom3i  9512  unwdomg  9513  xpwdomg  9514  unxpwdom  9518  infdifsn  9586  infdiffi  9587  isnum2  9874  wdomfil  9990  djuen  10099  djuenun  10100  djudom2  10113  djuxpdom  10115  djuinf  10118  infdju1  10119  pwdjuidm  10121  djulepw  10122  infdjuabs  10134  infdif  10137  pwdjudom  10144  infpss  10145  infmap2  10146  fictb  10173  infpssALT  10242  enfin2i  10250  fin34  10319  fodomb  10455  wdomac  10456  iundom2g  10469  iundom  10471  sdomsdomcard  10489  infxpidm  10491  engch  10557  fpwwe2lem3  10562  canthp1lem1  10581  canthp1lem2  10582  canthp1  10583  pwfseq  10593  pwxpndom2  10594  pwxpndom  10595  pwdjundom  10596  hargch  10602  gchaclem  10607  hasheni  14289  hashdomi  14321  clim  15436  rlim  15437  ntrivcvgn0  15840  ssc1  17763  ssc2  17764  ssctr  17767  frgpnabl  19789  dprddomprc  19916  dprdval  19919  dprdgrp  19921  dprdf  19922  dprdssv  19932  subgdmdprd  19950  dprd2da  19958  1stcrestlem  23372  hauspwdom  23421  isref  23429  ufilen  23850  dvle  25945  ellpi  33337  locfinref  33824  isfne4  36321  fnetr  36332  topfneec  36336  fnessref  36338  refssfne  36339  bj-epelb  37050  bj-idreseq  37143  phpreu  37591  sdomne0  43395  sdomne0d  43396  rn1st  45260  climf  45613  climf2  45657  iinfssc  49039  fuco21  49318  fucoid  49330