Theorem brrelex2i 5681

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440   class class class wbr 5098  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-rel 5631

This theorem is referenced by:  vtoclr  5687  brfvopabrbr  6938  domdifsn  8990  undom  8995  xpdom2  9002  xpdom1g  9004  domunsncan  9007  enfixsn  9016  fodomr  9058  pwdom  9059  domssex  9068  xpen  9070  mapdom1  9072  mapdom2  9078  pwen  9080  domtrfil  9118  sucdom2  9129  0sdom1dom  9148  1sdom2dom  9156  unxpdom  9161  unxpdom2  9162  sucxpdom  9163  isfinite2  9200  infn0ALT  9205  fin2inf  9206  fodomfir  9230  suppeqfsuppbi  9284  fsuppsssupp  9286  fsuppssov1  9289  fsuppunbi  9294  funsnfsupp  9297  mapfien2  9314  wemapso2  9460  card2on  9461  elharval  9468  harword  9470  brwdomi  9475  brwdomn0  9476  domwdom  9481  wdomtr  9482  wdompwdom  9485  canthwdom  9486  brwdom3i  9490  unwdomg  9491  xpwdomg  9492  unxpwdom  9496  infdifsn  9568  infdiffi  9569  isnum2  9859  wdomfil  9973  djuen  10082  djuenun  10083  djudom2  10096  djuxpdom  10098  djuinf  10101  infdju1  10102  pwdjuidm  10104  djulepw  10105  infdjuabs  10117  infdif  10120  pwdjudom  10127  infpss  10128  infmap2  10129  fictb  10156  infpssALT  10225  enfin2i  10233  fin34  10302  fodomb  10438  wdomac  10439  iundom2g  10452  iundom  10454  sdomsdomcard  10472  infxpidm  10474  engch  10541  fpwwe2lem3  10546  canthp1lem1  10565  canthp1lem2  10566  canthp1  10567  pwfseq  10577  pwxpndom2  10578  pwxpndom  10579  pwdjundom  10580  hargch  10586  gchaclem  10591  hasheni  14273  hashdomi  14305  clim  15419  rlim  15420  ntrivcvgn0  15823  ssc1  17747  ssc2  17748  ssctr  17751  frgpnabl  19806  dprddomprc  19933  dprdval  19936  dprdgrp  19938  dprdf  19939  dprdssv  19949  subgdmdprd  19967  dprd2da  19975  1stcrestlem  23398  hauspwdom  23447  isref  23455  ufilen  23876  dvle  25970  ellpi  33456  finextfldext  33823  locfinref  34000  isfne4  36536  fnetr  36547  topfneec  36551  fnessref  36553  refssfne  36554  bj-epelb  37272  bj-idreseq  37369  phpreu  37807  sdomne0  43675  sdomne0d  43676  rn1st  45538  climf  45889  climf2  45931  iinfssc  49323  fuco21  49602  fucoid  49614