Theorem brrelex2i 5688

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   class class class wbr 5085  Rel wrel 5636

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  vtoclr  5694  brfvopabrbr  6944  domdifsn  8998  undom  9003  xpdom2  9010  xpdom1g  9012  domunsncan  9015  enfixsn  9024  fodomr  9066  pwdom  9067  domssex  9076  xpen  9078  mapdom1  9080  mapdom2  9086  pwen  9088  domtrfil  9126  sucdom2  9137  0sdom1dom  9156  1sdom2dom  9164  unxpdom  9169  unxpdom2  9170  sucxpdom  9171  isfinite2  9208  infn0ALT  9213  fin2inf  9214  fodomfir  9238  suppeqfsuppbi  9292  fsuppsssupp  9294  fsuppssov1  9297  fsuppunbi  9302  funsnfsupp  9305  mapfien2  9322  wemapso2  9468  card2on  9469  elharval  9476  harword  9478  brwdomi  9483  brwdomn0  9484  domwdom  9489  wdomtr  9490  wdompwdom  9493  canthwdom  9494  brwdom3i  9498  unwdomg  9499  xpwdomg  9500  unxpwdom  9504  infdifsn  9578  infdiffi  9579  isnum2  9869  wdomfil  9983  djuen  10092  djuenun  10093  djudom2  10106  djuxpdom  10108  djuinf  10111  infdju1  10112  pwdjuidm  10114  djulepw  10115  infdjuabs  10127  infdif  10130  pwdjudom  10137  infpss  10138  infmap2  10139  fictb  10166  infpssALT  10235  enfin2i  10243  fin34  10312  fodomb  10448  wdomac  10449  iundom2g  10462  iundom  10464  sdomsdomcard  10482  infxpidm  10484  engch  10551  fpwwe2lem3  10556  canthp1lem1  10575  canthp1lem2  10576  canthp1  10577  pwfseq  10587  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  hargch  10596  gchaclem  10601  hasheni  14310  hashdomi  14342  clim  15456  rlim  15457  ntrivcvgn0  15863  ssc1  17788  ssc2  17789  ssctr  17792  frgpnabl  19850  dprddomprc  19977  dprdval  19980  dprdgrp  19982  dprdf  19983  dprdssv  19993  subgdmdprd  20011  dprd2da  20019  1stcrestlem  23417  hauspwdom  23466  isref  23474  ufilen  23895  dvle  25974  ellpi  33433  finextfldext  33808  locfinref  33985  isfne4  36522  fnetr  36533  topfneec  36537  fnessref  36539  refssfne  36540  bj-epelb  37376  bj-idreseq  37476  phpreu  37925  sdomne0  43840  sdomne0d  43841  rn1st  45702  climf  46052  climf2  46094  iinfssc  49532  fuco21  49811  fucoid  49823