Theorem brrelex2i 5739

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3473   class class class wbr 5152  Rel wrel 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-br 5153  df-opab 5215  df-xp 5688  df-rel 5689

This theorem is referenced by:  vtoclr  5745  brfvopabrbr  7007  brdomiOLD  8986  domdifsn  9085  undom  9090  undomOLD  9091  xpdom2  9098  xpdom1g  9100  domunsncan  9103  enfixsn  9112  sucdom2OLD  9113  fodomr  9159  pwdom  9160  domssex  9169  xpen  9171  mapdom1  9173  mapdom2  9179  pwen  9181  domtrfil  9226  sucdom2  9237  0sdom1dom  9269  1sdom2dom  9278  unxpdom  9284  unxpdom2  9285  sucxpdom  9286  isfinite2  9332  infn0ALT  9339  fin2inf  9340  suppeqfsuppbi  9410  fsuppsssupp  9412  fsuppssov1  9415  fsuppunbi  9420  funsnfsupp  9423  mapfien2  9440  wemapso2  9584  card2on  9585  elharval  9592  harword  9594  brwdomi  9599  brwdomn0  9600  domwdom  9605  wdomtr  9606  wdompwdom  9609  canthwdom  9610  brwdom3i  9614  unwdomg  9615  xpwdomg  9616  unxpwdom  9620  infdifsn  9688  infdiffi  9689  isnum2  9976  wdomfil  10092  djuen  10200  djuenun  10201  djudom2  10214  djuxpdom  10216  djuinf  10219  infdju1  10220  pwdjuidm  10222  djulepw  10223  infdjuabs  10237  infdif  10240  pwdjudom  10247  infpss  10248  infmap2  10249  fictb  10276  infpssALT  10344  enfin2i  10352  fin34  10421  fodomb  10557  wdomac  10558  iundom2g  10571  iundom  10573  sdomsdomcard  10591  infxpidm  10593  engch  10659  fpwwe2lem3  10664  canthp1lem1  10683  canthp1lem2  10684  canthp1  10685  pwfseq  10695  pwxpndom2  10696  pwxpndom  10697  pwdjundom  10698  hargch  10704  gchaclem  10709  hasheni  14347  hashdomi  14379  clim  15478  rlim  15479  ntrivcvgn0  15884  ssc1  17811  ssc2  17812  ssctr  17815  frgpnabl  19837  dprddomprc  19964  dprdval  19967  dprdgrp  19969  dprdf  19970  dprdssv  19980  subgdmdprd  19998  dprd2da  20006  1stcrestlem  23376  hauspwdom  23425  isref  23433  ufilen  23854  dvle  25960  ellpi  33110  locfinref  33475  isfne4  35857  fnetr  35868  topfneec  35872  fnessref  35874  refssfne  35875  bj-epelb  36581  bj-idreseq  36674  phpreu  37110  sdomne0  42874  sdomne0d  42875  rn1st  44679  climf  45039  climf2  45083