Theorem brrelex2i 5757

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488   class class class wbr 5166  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  vtoclr  5763  brfvopabrbr  7026  brdomiOLD  9019  domdifsn  9120  undom  9125  undomOLD  9126  xpdom2  9133  xpdom1g  9135  domunsncan  9138  enfixsn  9147  sucdom2OLD  9148  fodomr  9194  pwdom  9195  domssex  9204  xpen  9206  mapdom1  9208  mapdom2  9214  pwen  9216  domtrfil  9258  sucdom2  9269  0sdom1dom  9301  1sdom2dom  9310  unxpdom  9316  unxpdom2  9317  sucxpdom  9318  isfinite2  9362  infn0ALT  9369  fin2inf  9370  fodomfir  9396  suppeqfsuppbi  9448  fsuppsssupp  9450  fsuppssov1  9453  fsuppunbi  9458  funsnfsupp  9461  mapfien2  9478  wemapso2  9622  card2on  9623  elharval  9630  harword  9632  brwdomi  9637  brwdomn0  9638  domwdom  9643  wdomtr  9644  wdompwdom  9647  canthwdom  9648  brwdom3i  9652  unwdomg  9653  xpwdomg  9654  unxpwdom  9658  infdifsn  9726  infdiffi  9727  isnum2  10014  wdomfil  10130  djuen  10239  djuenun  10240  djudom2  10253  djuxpdom  10255  djuinf  10258  infdju1  10259  pwdjuidm  10261  djulepw  10262  infdjuabs  10274  infdif  10277  pwdjudom  10284  infpss  10285  infmap2  10286  fictb  10313  infpssALT  10382  enfin2i  10390  fin34  10459  fodomb  10595  wdomac  10596  iundom2g  10609  iundom  10611  sdomsdomcard  10629  infxpidm  10631  engch  10697  fpwwe2lem3  10702  canthp1lem1  10721  canthp1lem2  10722  canthp1  10723  pwfseq  10733  pwxpndom2  10734  pwxpndom  10735  pwdjundom  10736  hargch  10742  gchaclem  10747  hasheni  14397  hashdomi  14429  clim  15540  rlim  15541  ntrivcvgn0  15946  ssc1  17882  ssc2  17883  ssctr  17886  frgpnabl  19917  dprddomprc  20044  dprdval  20047  dprdgrp  20049  dprdf  20050  dprdssv  20060  subgdmdprd  20078  dprd2da  20086  1stcrestlem  23481  hauspwdom  23530  isref  23538  ufilen  23959  dvle  26066  ellpi  33366  locfinref  33787  isfne4  36306  fnetr  36317  topfneec  36321  fnessref  36323  refssfne  36324  bj-epelb  37035  bj-idreseq  37128  phpreu  37564  sdomne0  43375  sdomne0d  43376  rn1st  45183  climf  45543  climf2  45587