Theorem brrelex2i 5695

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447   class class class wbr 5107  Rel wrel 5643

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  vtoclr  5701  brfvopabrbr  6965  domdifsn  9024  undom  9029  xpdom2  9036  xpdom1g  9038  domunsncan  9041  enfixsn  9050  fodomr  9092  pwdom  9093  domssex  9102  xpen  9104  mapdom1  9106  mapdom2  9112  pwen  9114  domtrfil  9156  sucdom2  9167  0sdom1dom  9185  1sdom2dom  9194  unxpdom  9200  unxpdom2  9201  sucxpdom  9202  isfinite2  9245  infn0ALT  9252  fin2inf  9253  fodomfir  9279  suppeqfsuppbi  9330  fsuppsssupp  9332  fsuppssov1  9335  fsuppunbi  9340  funsnfsupp  9343  mapfien2  9360  wemapso2  9506  card2on  9507  elharval  9514  harword  9516  brwdomi  9521  brwdomn0  9522  domwdom  9527  wdomtr  9528  wdompwdom  9531  canthwdom  9532  brwdom3i  9536  unwdomg  9537  xpwdomg  9538  unxpwdom  9542  infdifsn  9610  infdiffi  9611  isnum2  9898  wdomfil  10014  djuen  10123  djuenun  10124  djudom2  10137  djuxpdom  10139  djuinf  10142  infdju1  10143  pwdjuidm  10145  djulepw  10146  infdjuabs  10158  infdif  10161  pwdjudom  10168  infpss  10169  infmap2  10170  fictb  10197  infpssALT  10266  enfin2i  10274  fin34  10343  fodomb  10479  wdomac  10480  iundom2g  10493  iundom  10495  sdomsdomcard  10513  infxpidm  10515  engch  10581  fpwwe2lem3  10586  canthp1lem1  10605  canthp1lem2  10606  canthp1  10607  pwfseq  10617  pwxpndom2  10618  pwxpndom  10619  pwdjundom  10620  hargch  10626  gchaclem  10631  hasheni  14313  hashdomi  14345  clim  15460  rlim  15461  ntrivcvgn0  15864  ssc1  17783  ssc2  17784  ssctr  17787  frgpnabl  19805  dprddomprc  19932  dprdval  19935  dprdgrp  19937  dprdf  19938  dprdssv  19948  subgdmdprd  19966  dprd2da  19974  1stcrestlem  23339  hauspwdom  23388  isref  23396  ufilen  23817  dvle  25912  ellpi  33344  locfinref  33831  isfne4  36328  fnetr  36339  topfneec  36343  fnessref  36345  refssfne  36346  bj-epelb  37057  bj-idreseq  37150  phpreu  37598  sdomne0  43402  sdomne0d  43403  rn1st  45267  climf  45620  climf2  45664  iinfssc  49046  fuco21  49325  fucoid  49337