Theorem brrelex2i 5718

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   class class class wbr 5109  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668

This theorem is referenced by:  vtoclr  5724  brfvopabrbr  6986  domdifsn  9044  undom  9049  xpdom2  9056  xpdom1g  9058  domunsncan  9061  enfixsn  9070  fodomr  9112  pwdom  9113  domssex  9122  xpen  9124  mapdom1  9126  mapdom2  9132  pwen  9134  domtrfil  9172  sucdom2  9183  0sdom1dom  9202  1sdom2dom  9210  unxpdom  9215  unxpdom2  9216  sucxpdom  9217  isfinite2  9254  infn0ALT  9259  fin2inf  9260  fodomfir  9283  suppeqfsuppbi  9335  fsuppsssupp  9337  fsuppssov1  9340  fsuppunbi  9345  funsnfsupp  9348  mapfien2  9365  wemapso2  9511  card2on  9512  elharval  9519  harword  9521  brwdomi  9526  brwdomn0  9527  domwdom  9532  wdomtr  9533  wdompwdom  9536  canthwdom  9537  brwdom3i  9541  unwdomg  9542  xpwdomg  9543  unxpwdom  9547  infdifsn  9622  infdiffi  9623  isnum2  9927  wdomfil  10041  djuen  10149  djuenun  10150  djudom2  10163  djuxpdom  10165  djuinf  10168  infdju1  10169  pwdjuidm  10171  djulepw  10172  infdjuabs  10184  infdif  10187  pwdjudom  10194  infpss  10195  infmap2  10196  fictb  10223  infpssALT  10292  enfin2i  10300  fin34  10369  fodomb  10505  wdomac  10506  iundom2g  10519  iundom  10521  sdomsdomcard  10539  infxpidm  10541  engch  10608  fpwwe2lem3  10613  canthp1lem1  10632  canthp1lem2  10633  canthp1  10634  pwfseq  10644  pwxpndom2  10645  pwxpndom  10646  pwdjundom  10647  hargch  10653  gchaclem  10658  hasheni  14380  hashdomi  14412  clim  15541  rlim  15542  ntrivcvgn0  15948  ssc1  17873  ssc2  17874  ssctr  17877  frgpnabl  19940  dprddomprc  20067  dprdval  20070  dprdgrp  20072  dprdf  20073  dprdssv  20083  subgdmdprd  20101  dprd2da  20109  1stcrestlem  23609  hauspwdom  23658  isref  23666  ufilen  24087  dvle  26166  ellpi  33687  finextfldext  34054  locfinref  34231  karddom  35574  kardsdom  35575  isfne4  36871  fnetr  36882  topfneec  36886  fnessref  36888  refssfne  36889  bj-epelb  37725  bj-idreseq  37826  phpreu  38275  sdomne0  44159  sdomne0d  44160  rn1st  46008  climf  46358  climf2  46400  iinfssc  49855  fuco21  50134  fucoid  50146