Theorem brrelex2i 5742

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480   class class class wbr 5143  Rel wrel 5690

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  vtoclr  5748  brfvopabrbr  7013  brdomiOLD  9000  domdifsn  9094  undom  9099  undomOLD  9100  xpdom2  9107  xpdom1g  9109  domunsncan  9112  enfixsn  9121  sucdom2OLD  9122  fodomr  9168  pwdom  9169  domssex  9178  xpen  9180  mapdom1  9182  mapdom2  9188  pwen  9190  domtrfil  9232  sucdom2  9243  0sdom1dom  9274  1sdom2dom  9283  unxpdom  9289  unxpdom2  9290  sucxpdom  9291  isfinite2  9334  infn0ALT  9341  fin2inf  9342  fodomfir  9368  suppeqfsuppbi  9419  fsuppsssupp  9421  fsuppssov1  9424  fsuppunbi  9429  funsnfsupp  9432  mapfien2  9449  wemapso2  9593  card2on  9594  elharval  9601  harword  9603  brwdomi  9608  brwdomn0  9609  domwdom  9614  wdomtr  9615  wdompwdom  9618  canthwdom  9619  brwdom3i  9623  unwdomg  9624  xpwdomg  9625  unxpwdom  9629  infdifsn  9697  infdiffi  9698  isnum2  9985  wdomfil  10101  djuen  10210  djuenun  10211  djudom2  10224  djuxpdom  10226  djuinf  10229  infdju1  10230  pwdjuidm  10232  djulepw  10233  infdjuabs  10245  infdif  10248  pwdjudom  10255  infpss  10256  infmap2  10257  fictb  10284  infpssALT  10353  enfin2i  10361  fin34  10430  fodomb  10566  wdomac  10567  iundom2g  10580  iundom  10582  sdomsdomcard  10600  infxpidm  10602  engch  10668  fpwwe2lem3  10673  canthp1lem1  10692  canthp1lem2  10693  canthp1  10694  pwfseq  10704  pwxpndom2  10705  pwxpndom  10706  pwdjundom  10707  hargch  10713  gchaclem  10718  hasheni  14387  hashdomi  14419  clim  15530  rlim  15531  ntrivcvgn0  15934  ssc1  17865  ssc2  17866  ssctr  17869  frgpnabl  19893  dprddomprc  20020  dprdval  20023  dprdgrp  20025  dprdf  20026  dprdssv  20036  subgdmdprd  20054  dprd2da  20062  1stcrestlem  23460  hauspwdom  23509  isref  23517  ufilen  23938  dvle  26046  ellpi  33401  locfinref  33840  isfne4  36341  fnetr  36352  topfneec  36356  fnessref  36358  refssfne  36359  bj-epelb  37070  bj-idreseq  37163  phpreu  37611  sdomne0  43426  sdomne0d  43427  rn1st  45280  climf  45637  climf2  45681  fuco21  49031  fucoid  49043