Theorem brrelex2i 5676

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436   class class class wbr 5092  Rel wrel 5624

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-rel 5626

This theorem is referenced by:  vtoclr  5682  brfvopabrbr  6927  domdifsn  8977  undom  8982  xpdom2  8989  xpdom1g  8991  domunsncan  8994  enfixsn  9003  fodomr  9045  pwdom  9046  domssex  9055  xpen  9057  mapdom1  9059  mapdom2  9065  pwen  9067  domtrfil  9106  sucdom2  9117  0sdom1dom  9135  1sdom2dom  9143  unxpdom  9148  unxpdom2  9149  sucxpdom  9150  isfinite2  9187  infn0ALT  9192  fin2inf  9193  fodomfir  9218  suppeqfsuppbi  9269  fsuppsssupp  9271  fsuppssov1  9274  fsuppunbi  9279  funsnfsupp  9282  mapfien2  9299  wemapso2  9445  card2on  9446  elharval  9453  harword  9455  brwdomi  9460  brwdomn0  9461  domwdom  9466  wdomtr  9467  wdompwdom  9470  canthwdom  9471  brwdom3i  9475  unwdomg  9476  xpwdomg  9477  unxpwdom  9481  infdifsn  9553  infdiffi  9554  isnum2  9841  wdomfil  9955  djuen  10064  djuenun  10065  djudom2  10078  djuxpdom  10080  djuinf  10083  infdju1  10084  pwdjuidm  10086  djulepw  10087  infdjuabs  10099  infdif  10102  pwdjudom  10109  infpss  10110  infmap2  10111  fictb  10138  infpssALT  10207  enfin2i  10215  fin34  10284  fodomb  10420  wdomac  10421  iundom2g  10434  iundom  10436  sdomsdomcard  10454  infxpidm  10456  engch  10522  fpwwe2lem3  10527  canthp1lem1  10546  canthp1lem2  10547  canthp1  10548  pwfseq  10558  pwxpndom2  10559  pwxpndom  10560  pwdjundom  10561  hargch  10567  gchaclem  10572  hasheni  14255  hashdomi  14287  clim  15401  rlim  15402  ntrivcvgn0  15805  ssc1  17728  ssc2  17729  ssctr  17732  frgpnabl  19754  dprddomprc  19881  dprdval  19884  dprdgrp  19886  dprdf  19887  dprdssv  19897  subgdmdprd  19915  dprd2da  19923  1stcrestlem  23337  hauspwdom  23386  isref  23394  ufilen  23815  dvle  25910  ellpi  33311  finextfldext  33637  locfinref  33814  isfne4  36324  fnetr  36335  topfneec  36339  fnessref  36341  refssfne  36342  bj-epelb  37053  bj-idreseq  37146  phpreu  37594  sdomne0  43396  sdomne0d  43397  rn1st  45261  climf  45613  climf2  45657  iinfssc  49052  fuco21  49331  fucoid  49343