Theorem brrelex2i 5159

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

Syntax hints:   → wi 4   ∈ wcel 1990  Vcvv 3200   class class class wbr 4653  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-rel 5121

This theorem is referenced by:  vtoclr  5164  brfvopabrbr  6279  brdomi  7966  domdifsn  8043  undom  8048  xpdom2  8055  xpdom1g  8057  domunsncan  8060  enfixsn  8069  fodomr  8111  pwdom  8112  domssex  8121  xpen  8123  mapdom1  8125  mapdom2  8131  pwen  8133  sucdom2  8156  unxpdom  8167  unxpdom2  8168  sucxpdom  8169  isfinite2  8218  infn0  8222  fin2inf  8223  fsuppimp  8281  suppeqfsuppbi  8289  fsuppsssupp  8291  fsuppunbi  8296  funsnfsupp  8299  mapfien2  8314  wemapso2  8458  card2on  8459  elharval  8468  harword  8470  brwdomi  8473  brwdomn0  8474  domwdom  8479  wdomtr  8480  wdompwdom  8483  canthwdom  8484  brwdom3i  8488  unwdomg  8489  xpwdomg  8490  unxpwdom  8494  infdifsn  8554  infdiffi  8555  isnum2  8771  wdomfil  8884  cdaen  8995  cdaenun  8996  cdadom1  9008  cdaxpdom  9011  cdainf  9014  infcda1  9015  pwcdaidm  9017  cdalepw  9018  infpss  9039  infmap2  9040  fictb  9067  infpssALT  9135  enfin2i  9143  fin34  9212  fodomb  9348  wdomac  9349  iundom2g  9362  iundom  9364  sdomsdomcard  9382  infxpidm  9384  engch  9450  fpwwe2lem3  9455  canthp1lem1  9474  canthp1lem2  9475  canthp1  9476  pwfseq  9486  pwxpndom2  9487  pwxpndom  9488  pwcdandom  9489  hargch  9495  gchaclem  9500  hasheni  13136  hashdomi  13169  brfi1indALT  13282  brfi1indALTOLD  13288  clim  14225  rlim  14226  ntrivcvgn0  14630  ssc1  16481  ssc2  16482  ssctr  16485  frgpnabl  18278  dprddomprc  18399  dprdval  18402  dprdgrp  18404  dprdf  18405  dprdssv  18415  subgdmdprd  18433  dprd2da  18441  1stcrestlem  21255  hauspwdom  21304  isref  21312  ufilen  21734  dvle  23770  subgrv  26162  locfinref  29908  isfne4  32335  fnetr  32346  topfneec  32350  fnessref  32352  refssfne  32353  phpreu  33393  climf  39854  climf2  39898  linindsv  42234