Theorem brrelex2i 5604

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

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3495   class class class wbr 5059  Rel wrel 5555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-br 5060  df-opab 5122  df-xp 5556  df-rel 5557

This theorem is referenced by:  vtoclr  5610  brfvopabrbr  6760  brdomi  8514  domdifsn  8594  undom  8599  xpdom2  8606  xpdom1g  8608  domunsncan  8611  enfixsn  8620  fodomr  8662  pwdom  8663  domssex  8672  xpen  8674  mapdom1  8676  mapdom2  8682  pwen  8684  sucdom2  8708  unxpdom  8719  unxpdom2  8720  sucxpdom  8721  isfinite2  8770  infn0  8774  fin2inf  8775  suppeqfsuppbi  8841  fsuppsssupp  8843  fsuppunbi  8848  funsnfsupp  8851  mapfien2  8866  wemapso2  9011  card2on  9012  elharval  9021  harword  9023  brwdomi  9026  brwdomn0  9027  domwdom  9032  wdomtr  9033  wdompwdom  9036  canthwdom  9037  brwdom3i  9041  unwdomg  9042  xpwdomg  9043  unxpwdom  9047  infdifsn  9114  infdiffi  9115  isnum2  9368  wdomfil  9481  djuen  9589  djuenun  9590  djudom2  9603  djuxpdom  9605  djuinf  9608  infdju1  9609  pwdjuidm  9611  djulepw  9612  infdjuabs  9622  infdif  9625  pwdjudom  9632  infpss  9633  infmap2  9634  fictb  9661  infpssALT  9729  enfin2i  9737  fin34  9806  fodomb  9942  wdomac  9943  iundom2g  9956  iundom  9958  sdomsdomcard  9976  infxpidm  9978  engch  10044  fpwwe2lem3  10049  canthp1lem1  10068  canthp1lem2  10069  canthp1  10070  pwfseq  10080  pwxpndom2  10081  pwxpndom  10082  pwdjundom  10083  hargch  10089  gchaclem  10094  hasheni  13702  hashdomi  13735  brfi1indALT  13852  clim  14845  rlim  14846  ntrivcvgn0  15248  ssc1  17085  ssc2  17086  ssctr  17089  frgpnabl  18989  dprddomprc  19116  dprdval  19119  dprdgrp  19121  dprdf  19122  dprdssv  19132  subgdmdprd  19150  dprd2da  19158  1stcrestlem  22054  hauspwdom  22103  isref  22111  ufilen  22532  dvle  24598  locfinref  31100  isfne4  33683  fnetr  33694  topfneec  33698  fnessref  33700  refssfne  33701  bj-epelb  34355  bj-idreseq  34448  phpreu  34870  climf  41895  climf2  41939