Theorem brrelex2i 5609

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494   class class class wbr 5066  Rel wrel 5560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-rel 5562

This theorem is referenced by:  vtoclr  5615  brfvopabrbr  6765  brdomi  8520  domdifsn  8600  undom  8605  xpdom2  8612  xpdom1g  8614  domunsncan  8617  enfixsn  8626  fodomr  8668  pwdom  8669  domssex  8678  xpen  8680  mapdom1  8682  mapdom2  8688  pwen  8690  sucdom2  8714  unxpdom  8725  unxpdom2  8726  sucxpdom  8727  isfinite2  8776  infn0  8780  fin2inf  8781  suppeqfsuppbi  8847  fsuppsssupp  8849  fsuppunbi  8854  funsnfsupp  8857  mapfien2  8872  wemapso2  9017  card2on  9018  elharval  9027  harword  9029  brwdomi  9032  brwdomn0  9033  domwdom  9038  wdomtr  9039  wdompwdom  9042  canthwdom  9043  brwdom3i  9047  unwdomg  9048  xpwdomg  9049  unxpwdom  9053  infdifsn  9120  infdiffi  9121  isnum2  9374  wdomfil  9487  djuen  9595  djuenun  9596  djudom2  9609  djuxpdom  9611  djuinf  9614  infdju1  9615  pwdjuidm  9617  djulepw  9618  infdjuabs  9628  infdif  9631  pwdjudom  9638  infpss  9639  infmap2  9640  fictb  9667  infpssALT  9735  enfin2i  9743  fin34  9812  fodomb  9948  wdomac  9949  iundom2g  9962  iundom  9964  sdomsdomcard  9982  infxpidm  9984  engch  10050  fpwwe2lem3  10055  canthp1lem1  10074  canthp1lem2  10075  canthp1  10076  pwfseq  10086  pwxpndom2  10087  pwxpndom  10088  pwdjundom  10089  hargch  10095  gchaclem  10100  hasheni  13709  hashdomi  13742  brfi1indALT  13859  clim  14851  rlim  14852  ntrivcvgn0  15254  ssc1  17091  ssc2  17092  ssctr  17095  frgpnabl  18995  dprddomprc  19122  dprdval  19125  dprdgrp  19127  dprdf  19128  dprdssv  19138  subgdmdprd  19156  dprd2da  19164  1stcrestlem  22060  hauspwdom  22109  isref  22117  ufilen  22538  dvle  24604  locfinref  31105  isfne4  33688  fnetr  33699  topfneec  33703  fnessref  33705  refssfne  33706  bj-epelb  34364  bj-idreseq  34457  phpreu  34891  climf  41923  climf2  41967