Theorem brrelex2i 5731

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3474   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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  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  5737  brfvopabrbr  6992  brdomiOLD  8951  domdifsn  9050  undom  9055  undomOLD  9056  xpdom2  9063  xpdom1g  9065  domunsncan  9068  enfixsn  9077  sucdom2OLD  9078  fodomr  9124  pwdom  9125  domssex  9134  xpen  9136  mapdom1  9138  mapdom2  9144  pwen  9146  domtrfil  9191  sucdom2  9202  0sdom1dom  9234  1sdom2dom  9243  unxpdom  9249  unxpdom2  9250  sucxpdom  9251  isfinite2  9297  infn0ALT  9304  fin2inf  9305  suppeqfsuppbi  9373  fsuppsssupp  9375  fsuppunbi  9380  funsnfsupp  9383  mapfien2  9400  wemapso2  9544  card2on  9545  elharval  9552  harword  9554  brwdomi  9559  brwdomn0  9560  domwdom  9565  wdomtr  9566  wdompwdom  9569  canthwdom  9570  brwdom3i  9574  unwdomg  9575  xpwdomg  9576  unxpwdom  9580  infdifsn  9648  infdiffi  9649  isnum2  9936  wdomfil  10052  djuen  10160  djuenun  10161  djudom2  10174  djuxpdom  10176  djuinf  10179  infdju1  10180  pwdjuidm  10182  djulepw  10183  infdjuabs  10197  infdif  10200  pwdjudom  10207  infpss  10208  infmap2  10209  fictb  10236  infpssALT  10304  enfin2i  10312  fin34  10381  fodomb  10517  wdomac  10518  iundom2g  10531  iundom  10533  sdomsdomcard  10551  infxpidm  10553  engch  10619  fpwwe2lem3  10624  canthp1lem1  10643  canthp1lem2  10644  canthp1  10645  pwfseq  10655  pwxpndom2  10656  pwxpndom  10657  pwdjundom  10658  hargch  10664  gchaclem  10669  hasheni  14304  hashdomi  14336  clim  15434  rlim  15435  ntrivcvgn0  15840  ssc1  17764  ssc2  17765  ssctr  17768  frgpnabl  19737  dprddomprc  19864  dprdval  19867  dprdgrp  19869  dprdf  19870  dprdssv  19880  subgdmdprd  19898  dprd2da  19906  1stcrestlem  22947  hauspwdom  22996  isref  23004  ufilen  23425  dvle  25515  locfinref  32809  isfne4  35213  fnetr  35224  topfneec  35228  fnessref  35230  refssfne  35231  bj-epelb  35938  bj-idreseq  36031  phpreu  36460  sdomne0  42149  sdomne0d  42150  rn1st  43964  climf  44324  climf2  44368