Theorem brrelex2i 5711

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3459   class class class wbr 5119  Rel wrel 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  vtoclr  5717  brfvopabrbr  6982  brdomiOLD  8972  domdifsn  9066  undom  9071  undomOLD  9072  xpdom2  9079  xpdom1g  9081  domunsncan  9084  enfixsn  9093  sucdom2OLD  9094  fodomr  9140  pwdom  9141  domssex  9150  xpen  9152  mapdom1  9154  mapdom2  9160  pwen  9162  domtrfil  9204  sucdom2  9215  0sdom1dom  9244  1sdom2dom  9253  unxpdom  9259  unxpdom2  9260  sucxpdom  9261  isfinite2  9304  infn0ALT  9311  fin2inf  9312  fodomfir  9338  suppeqfsuppbi  9389  fsuppsssupp  9391  fsuppssov1  9394  fsuppunbi  9399  funsnfsupp  9402  mapfien2  9419  wemapso2  9565  card2on  9566  elharval  9573  harword  9575  brwdomi  9580  brwdomn0  9581  domwdom  9586  wdomtr  9587  wdompwdom  9590  canthwdom  9591  brwdom3i  9595  unwdomg  9596  xpwdomg  9597  unxpwdom  9601  infdifsn  9669  infdiffi  9670  isnum2  9957  wdomfil  10073  djuen  10182  djuenun  10183  djudom2  10196  djuxpdom  10198  djuinf  10201  infdju1  10202  pwdjuidm  10204  djulepw  10205  infdjuabs  10217  infdif  10220  pwdjudom  10227  infpss  10228  infmap2  10229  fictb  10256  infpssALT  10325  enfin2i  10333  fin34  10402  fodomb  10538  wdomac  10539  iundom2g  10552  iundom  10554  sdomsdomcard  10572  infxpidm  10574  engch  10640  fpwwe2lem3  10645  canthp1lem1  10664  canthp1lem2  10665  canthp1  10666  pwfseq  10676  pwxpndom2  10677  pwxpndom  10678  pwdjundom  10679  hargch  10685  gchaclem  10690  hasheni  14364  hashdomi  14396  clim  15508  rlim  15509  ntrivcvgn0  15912  ssc1  17832  ssc2  17833  ssctr  17836  frgpnabl  19854  dprddomprc  19981  dprdval  19984  dprdgrp  19986  dprdf  19987  dprdssv  19997  subgdmdprd  20015  dprd2da  20023  1stcrestlem  23388  hauspwdom  23437  isref  23445  ufilen  23866  dvle  25962  ellpi  33334  locfinref  33818  isfne4  36304  fnetr  36315  topfneec  36319  fnessref  36321  refssfne  36322  bj-epelb  37033  bj-idreseq  37126  phpreu  37574  sdomne0  43384  sdomne0d  43385  rn1st  45245  climf  45599  climf2  45643  iinfssc  48972  fuco21  49195  fucoid  49207