Theorem brrelex2i 5745

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477   class class class wbr 5147  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  vtoclr  5751  brfvopabrbr  7012  brdomiOLD  8998  domdifsn  9092  undom  9097  undomOLD  9098  xpdom2  9105  xpdom1g  9107  domunsncan  9110  enfixsn  9119  sucdom2OLD  9120  fodomr  9166  pwdom  9167  domssex  9176  xpen  9178  mapdom1  9180  mapdom2  9186  pwen  9188  domtrfil  9229  sucdom2  9240  0sdom1dom  9271  1sdom2dom  9280  unxpdom  9286  unxpdom2  9287  sucxpdom  9288  isfinite2  9331  infn0ALT  9338  fin2inf  9339  fodomfir  9365  suppeqfsuppbi  9416  fsuppsssupp  9418  fsuppssov1  9421  fsuppunbi  9426  funsnfsupp  9429  mapfien2  9446  wemapso2  9590  card2on  9591  elharval  9598  harword  9600  brwdomi  9605  brwdomn0  9606  domwdom  9611  wdomtr  9612  wdompwdom  9615  canthwdom  9616  brwdom3i  9620  unwdomg  9621  xpwdomg  9622  unxpwdom  9626  infdifsn  9694  infdiffi  9695  isnum2  9982  wdomfil  10098  djuen  10207  djuenun  10208  djudom2  10221  djuxpdom  10223  djuinf  10226  infdju1  10227  pwdjuidm  10229  djulepw  10230  infdjuabs  10242  infdif  10245  pwdjudom  10252  infpss  10253  infmap2  10254  fictb  10281  infpssALT  10350  enfin2i  10358  fin34  10427  fodomb  10563  wdomac  10564  iundom2g  10577  iundom  10579  sdomsdomcard  10597  infxpidm  10599  engch  10665  fpwwe2lem3  10670  canthp1lem1  10689  canthp1lem2  10690  canthp1  10691  pwfseq  10701  pwxpndom2  10702  pwxpndom  10703  pwdjundom  10704  hargch  10710  gchaclem  10715  hasheni  14383  hashdomi  14415  clim  15526  rlim  15527  ntrivcvgn0  15930  ssc1  17868  ssc2  17869  ssctr  17872  frgpnabl  19907  dprddomprc  20034  dprdval  20037  dprdgrp  20039  dprdf  20040  dprdssv  20050  subgdmdprd  20068  dprd2da  20076  1stcrestlem  23475  hauspwdom  23524  isref  23532  ufilen  23953  dvle  26060  ellpi  33380  locfinref  33801  isfne4  36322  fnetr  36333  topfneec  36337  fnessref  36339  refssfne  36340  bj-epelb  37051  bj-idreseq  37144  phpreu  37590  sdomne0  43402  sdomne0d  43403  rn1st  45218  climf  45577  climf2  45621