Theorem brrelex2i 5682

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3441   class class class wbr 5099  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5631  df-rel 5632

This theorem is referenced by:  vtoclr  5688  brfvopabrbr  6939  domdifsn  8992  undom  8997  xpdom2  9004  xpdom1g  9006  domunsncan  9009  enfixsn  9018  fodomr  9060  pwdom  9061  domssex  9070  xpen  9072  mapdom1  9074  mapdom2  9080  pwen  9082  domtrfil  9120  sucdom2  9131  0sdom1dom  9150  1sdom2dom  9158  unxpdom  9163  unxpdom2  9164  sucxpdom  9165  isfinite2  9202  infn0ALT  9207  fin2inf  9208  fodomfir  9232  suppeqfsuppbi  9286  fsuppsssupp  9288  fsuppssov1  9291  fsuppunbi  9296  funsnfsupp  9299  mapfien2  9316  wemapso2  9462  card2on  9463  elharval  9470  harword  9472  brwdomi  9477  brwdomn0  9478  domwdom  9483  wdomtr  9484  wdompwdom  9487  canthwdom  9488  brwdom3i  9492  unwdomg  9493  xpwdomg  9494  unxpwdom  9498  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  14275  hashdomi  14307  clim  15421  rlim  15422  ntrivcvgn0  15825  ssc1  17749  ssc2  17750  ssctr  17753  frgpnabl  19808  dprddomprc  19935  dprdval  19938  dprdgrp  19940  dprdf  19941  dprdssv  19951  subgdmdprd  19969  dprd2da  19977  1stcrestlem  23400  hauspwdom  23449  isref  23457  ufilen  23878  dvle  25972  ellpi  33435  finextfldext  33802  locfinref  33979  isfne4  36515  fnetr  36526  topfneec  36530  fnessref  36532  refssfne  36533  bj-epelb  37245  bj-idreseq  37338  phpreu  37776  sdomne0  43690  sdomne0d  43691  rn1st  45553  climf  45904  climf2  45946  iinfssc  49338  fuco21  49617  fucoid  49629