Theorem brrelex2i 5732

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

Syntax hints:   → wi 4   ∈ wcel 2104  Vcvv 3472   class class class wbr 5147  Rel wrel 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-rel 5682

This theorem is referenced by:  vtoclr  5738  brfvopabrbr  6994  brdomiOLD  8957  domdifsn  9056  undom  9061  undomOLD  9062  xpdom2  9069  xpdom1g  9071  domunsncan  9074  enfixsn  9083  sucdom2OLD  9084  fodomr  9130  pwdom  9131  domssex  9140  xpen  9142  mapdom1  9144  mapdom2  9150  pwen  9152  domtrfil  9197  sucdom2  9208  0sdom1dom  9240  1sdom2dom  9249  unxpdom  9255  unxpdom2  9256  sucxpdom  9257  isfinite2  9303  infn0ALT  9310  fin2inf  9311  suppeqfsuppbi  9379  fsuppsssupp  9381  fsuppunbi  9386  funsnfsupp  9389  mapfien2  9406  wemapso2  9550  card2on  9551  elharval  9558  harword  9560  brwdomi  9565  brwdomn0  9566  domwdom  9571  wdomtr  9572  wdompwdom  9575  canthwdom  9576  brwdom3i  9580  unwdomg  9581  xpwdomg  9582  unxpwdom  9586  infdifsn  9654  infdiffi  9655  isnum2  9942  wdomfil  10058  djuen  10166  djuenun  10167  djudom2  10180  djuxpdom  10182  djuinf  10185  infdju1  10186  pwdjuidm  10188  djulepw  10189  infdjuabs  10203  infdif  10206  pwdjudom  10213  infpss  10214  infmap2  10215  fictb  10242  infpssALT  10310  enfin2i  10318  fin34  10387  fodomb  10523  wdomac  10524  iundom2g  10537  iundom  10539  sdomsdomcard  10557  infxpidm  10559  engch  10625  fpwwe2lem3  10630  canthp1lem1  10649  canthp1lem2  10650  canthp1  10651  pwfseq  10661  pwxpndom2  10662  pwxpndom  10663  pwdjundom  10664  hargch  10670  gchaclem  10675  hasheni  14312  hashdomi  14344  clim  15442  rlim  15443  ntrivcvgn0  15848  ssc1  17772  ssc2  17773  ssctr  17776  frgpnabl  19784  dprddomprc  19911  dprdval  19914  dprdgrp  19916  dprdf  19917  dprdssv  19927  subgdmdprd  19945  dprd2da  19953  1stcrestlem  23176  hauspwdom  23225  isref  23233  ufilen  23654  dvle  25759  locfinref  33119  isfne4  35528  fnetr  35539  topfneec  35543  fnessref  35545  refssfne  35546  bj-epelb  36253  bj-idreseq  36346  phpreu  36775  sdomne0  42466  sdomne0d  42467  rn1st  44276  climf  44636  climf2  44680