Theorem brrelex2i 5459

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

Syntax hints:   → wi 4   ∈ wcel 2050  Vcvv 3415   class class class wbr 4929  Rel wrel 5412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-xp 5413  df-rel 5414

This theorem is referenced by:  vtoclr  5465  brfvopabrbr  6592  brdomi  8317  domdifsn  8396  undom  8401  xpdom2  8408  xpdom1g  8410  domunsncan  8413  enfixsn  8422  fodomr  8464  pwdom  8465  domssex  8474  xpen  8476  mapdom1  8478  mapdom2  8484  pwen  8486  sucdom2  8509  unxpdom  8520  unxpdom2  8521  sucxpdom  8522  isfinite2  8571  infn0  8575  fin2inf  8576  suppeqfsuppbi  8642  fsuppsssupp  8644  fsuppunbi  8649  funsnfsupp  8652  mapfien2  8667  wemapso2  8812  card2on  8813  elharval  8822  harword  8824  brwdomi  8827  brwdomn0  8828  domwdom  8833  wdomtr  8834  wdompwdom  8837  canthwdom  8838  brwdom3i  8842  unwdomg  8843  xpwdomg  8844  unxpwdom  8848  infdifsn  8914  infdiffi  8915  isnum2  9168  wdomfil  9281  djuen  9393  djuenun  9394  djudom2  9407  djuxpdom  9409  djuinf  9412  infdju1  9413  pwdjuidm  9415  djulepw  9416  infdjuabs  9426  infdif  9429  pwdjudom  9436  infpss  9437  infmap2  9438  fictb  9465  infpssALT  9533  enfin2i  9541  fin34  9610  fodomb  9746  wdomac  9747  iundom2g  9760  iundom  9762  sdomsdomcard  9780  infxpidm  9782  engch  9848  fpwwe2lem3  9853  canthp1lem1  9872  canthp1lem2  9873  canthp1  9874  pwfseq  9884  pwxpndom2  9885  pwxpndom  9886  pwdjundom  9887  hargch  9893  gchaclem  9898  hasheni  13523  hashdomi  13554  brfi1indALT  13669  clim  14712  rlim  14713  ntrivcvgn0  15114  ssc1  16949  ssc2  16950  ssctr  16953  frgpnabl  18751  dprddomprc  18872  dprdval  18875  dprdgrp  18877  dprdf  18878  dprdssv  18888  subgdmdprd  18906  dprd2da  18914  1stcrestlem  21764  hauspwdom  21813  isref  21821  ufilen  22242  dvle  24307  locfinref  30755  isfne4  33215  fnetr  33226  topfneec  33230  fnessref  33232  refssfne  33233  bj-elep  33875  phpreu  34323  climf  41340  climf2  41384