Theorem brrelex2i 5734

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   class class class wbr 5149  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-rel 5684

This theorem is referenced by:  vtoclr  5740  brfvopabrbr  6996  brdomiOLD  8955  domdifsn  9054  undom  9059  undomOLD  9060  xpdom2  9067  xpdom1g  9069  domunsncan  9072  enfixsn  9081  sucdom2OLD  9082  fodomr  9128  pwdom  9129  domssex  9138  xpen  9140  mapdom1  9142  mapdom2  9148  pwen  9150  domtrfil  9195  sucdom2  9206  0sdom1dom  9238  1sdom2dom  9247  unxpdom  9253  unxpdom2  9254  sucxpdom  9255  isfinite2  9301  infn0ALT  9308  fin2inf  9309  suppeqfsuppbi  9377  fsuppsssupp  9379  fsuppunbi  9384  funsnfsupp  9387  mapfien2  9404  wemapso2  9548  card2on  9549  elharval  9556  harword  9558  brwdomi  9563  brwdomn0  9564  domwdom  9569  wdomtr  9570  wdompwdom  9573  canthwdom  9574  brwdom3i  9578  unwdomg  9579  xpwdomg  9580  unxpwdom  9584  infdifsn  9652  infdiffi  9653  isnum2  9940  wdomfil  10056  djuen  10164  djuenun  10165  djudom2  10178  djuxpdom  10180  djuinf  10183  infdju1  10184  pwdjuidm  10186  djulepw  10187  infdjuabs  10201  infdif  10204  pwdjudom  10211  infpss  10212  infmap2  10213  fictb  10240  infpssALT  10308  enfin2i  10316  fin34  10385  fodomb  10521  wdomac  10522  iundom2g  10535  iundom  10537  sdomsdomcard  10555  infxpidm  10557  engch  10623  fpwwe2lem3  10628  canthp1lem1  10647  canthp1lem2  10648  canthp1  10649  pwfseq  10659  pwxpndom2  10660  pwxpndom  10661  pwdjundom  10662  hargch  10668  gchaclem  10673  hasheni  14308  hashdomi  14340  clim  15438  rlim  15439  ntrivcvgn0  15844  ssc1  17768  ssc2  17769  ssctr  17772  frgpnabl  19743  dprddomprc  19870  dprdval  19873  dprdgrp  19875  dprdf  19876  dprdssv  19886  subgdmdprd  19904  dprd2da  19912  1stcrestlem  22956  hauspwdom  23005  isref  23013  ufilen  23434  dvle  25524  locfinref  32821  isfne4  35225  fnetr  35236  topfneec  35240  fnessref  35242  refssfne  35243  bj-epelb  35950  bj-idreseq  36043  phpreu  36472  sdomne0  42164  sdomne0d  42165  rn1st  43978  climf  44338  climf2  44382