Theorem brrelex2i 5705

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   class class class wbr 5101  Rel wrel 5653

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5247  ax-pr 5391

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5102  df-opab 5164  df-xp 5654  df-rel 5655

This theorem is referenced by:  vtoclr  5711  brfvopabrbr  6973  domdifsn  9033  undom  9038  xpdom2  9045  xpdom1g  9047  domunsncan  9050  enfixsn  9059  fodomr  9101  pwdom  9102  domssex  9111  xpen  9113  mapdom1  9115  mapdom2  9121  pwen  9123  domtrfil  9161  sucdom2  9172  0sdom1dom  9191  1sdom2dom  9199  unxpdom  9204  unxpdom2  9205  sucxpdom  9206  isfinite2  9243  infn0ALT  9248  fin2inf  9249  fodomfir  9273  suppeqfsuppbi  9326  fsuppsssupp  9328  fsuppssov1  9331  fsuppunbi  9336  funsnfsupp  9339  mapfien2  9356  wemapso2  9502  card2on  9503  elharval  9510  harword  9512  brwdomi  9517  brwdomn0  9518  domwdom  9523  wdomtr  9524  wdompwdom  9527  canthwdom  9528  brwdom3i  9532  unwdomg  9533  xpwdomg  9534  unxpwdom  9538  infdifsn  9613  infdiffi  9614  isnum2  9904  wdomfil  10018  djuen  10127  djuenun  10128  djudom2  10141  djuxpdom  10143  djuinf  10146  infdju1  10147  pwdjuidm  10149  djulepw  10150  infdjuabs  10162  infdif  10165  pwdjudom  10172  infpss  10173  infmap2  10174  fictb  10201  infpssALT  10271  enfin2i  10279  fin34  10348  fodomb  10484  wdomac  10485  iundom2g  10498  iundom  10500  sdomsdomcard  10518  infxpidm  10520  engch  10587  fpwwe2lem3  10592  canthp1lem1  10611  canthp1lem2  10612  canthp1  10613  pwfseq  10623  pwxpndom2  10624  pwxpndom  10625  pwdjundom  10626  hargch  10632  gchaclem  10637  hasheni  14362  hashdomi  14394  clim  15522  rlim  15523  ntrivcvgn0  15929  ssc1  17855  ssc2  17856  ssctr  17859  frgpnabl  19916  dprddomprc  20043  dprdval  20046  dprdgrp  20048  dprdf  20049  dprdssv  20059  subgdmdprd  20077  dprd2da  20085  1stcrestlem  23513  hauspwdom  23562  isref  23570  ufilen  23991  dvle  26070  ellpi  33560  finextfldext  33962  locfinref  34139  isfne4  36701  fnetr  36712  topfneec  36716  fnessref  36718  refssfne  36719  bj-epelb  37555  bj-idreseq  37655  phpreu  38104  sdomne0  43990  sdomne0d  43991  rn1st  45849  climf  46199  climf2  46241  iinfssc  49679  fuco21  49958  fucoid  49970