Theorem brrelex2i 5676

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431   class class class wbr 5073  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5219  ax-pr 5363

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-sn 4557  df-pr 4559  df-op 4563  df-br 5074  df-opab 5136  df-xp 5625  df-rel 5626

This theorem is referenced by:  vtoclr  5682  brfvopabrbr  6933  domdifsn  8989  undom  8994  xpdom2  9001  xpdom1g  9003  domunsncan  9006  enfixsn  9015  fodomr  9057  pwdom  9058  domssex  9067  xpen  9069  mapdom1  9071  mapdom2  9077  pwen  9079  domtrfil  9117  sucdom2  9128  0sdom1dom  9147  1sdom2dom  9155  unxpdom  9160  unxpdom2  9161  sucxpdom  9162  isfinite2  9199  infn0ALT  9204  fin2inf  9205  fodomfir  9229  suppeqfsuppbi  9283  fsuppsssupp  9285  fsuppssov1  9288  fsuppunbi  9293  funsnfsupp  9296  mapfien2  9313  wemapso2  9459  card2on  9460  elharval  9467  harword  9469  brwdomi  9474  brwdomn0  9475  domwdom  9480  wdomtr  9481  wdompwdom  9484  canthwdom  9485  brwdom3i  9489  unwdomg  9490  xpwdomg  9491  unxpwdom  9495  infdifsn  9570  infdiffi  9571  isnum2  9861  wdomfil  9975  djuen  10084  djuenun  10085  djudom2  10098  djuxpdom  10100  djuinf  10103  infdju1  10104  pwdjuidm  10106  djulepw  10107  infdjuabs  10119  infdif  10122  pwdjudom  10129  infpss  10130  infmap2  10131  fictb  10158  infpssALT  10227  enfin2i  10235  fin34  10304  fodomb  10440  wdomac  10441  iundom2g  10454  iundom  10456  sdomsdomcard  10474  infxpidm  10476  engch  10543  fpwwe2lem3  10548  canthp1lem1  10567  canthp1lem2  10568  canthp1  10569  pwfseq  10579  pwxpndom2  10580  pwxpndom  10581  pwdjundom  10582  hargch  10588  gchaclem  10593  hasheni  14302  hashdomi  14334  clim  15448  rlim  15449  ntrivcvgn0  15855  ssc1  17780  ssc2  17781  ssctr  17784  frgpnabl  19842  dprddomprc  19969  dprdval  19972  dprdgrp  19974  dprdf  19975  dprdssv  19985  subgdmdprd  20003  dprd2da  20011  1stcrestlem  23436  hauspwdom  23485  isref  23493  ufilen  23914  dvle  25993  ellpi  33457  finextfldext  33857  locfinref  34034  isfne4  36577  fnetr  36588  topfneec  36592  fnessref  36594  refssfne  36595  bj-epelb  37431  bj-idreseq  37531  phpreu  37980  sdomne0  43866  sdomne0d  43867  rn1st  45725  climf  46075  climf2  46117  iinfssc  49555  fuco21  49834  fucoid  49846