Theorem brrelex2i 5712

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   class class class wbr 5103  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662

This theorem is used by:  vtoclr  5718  brfvopabrbr  6984  domdifsn  9061  undom  9066  xpdom2  9073  xpdom1g  9075  domunsncan  9078  enfixsn  9087  fodomr  9129  pwdom  9130  domssex  9139  xpen  9141  mapdom1  9143  mapdom2  9149  pwen  9151  domtrfil  9189  sucdom2  9200  0sdom1dom  9219  1sdom2dom  9227  unxpdom  9232  unxpdom2  9233  sucxpdom  9234  isfinite2  9271  infn0ALT  9276  fin2inf  9277  fodomfir  9300  suppeqfsuppbi  9352  fsuppsssupp  9354  fsuppssov1  9357  fsuppunbi  9362  funsnfsupp  9365  mapfien2  9382  wemapso2  9528  card2on  9529  elharval  9536  harword  9538  brwdomi  9543  brwdomn0  9544  domwdom  9549  wdomtr  9550  wdompwdom  9553  canthwdom  9554  brwdom3i  9558  unwdomg  9559  xpwdomg  9560  unxpwdom  9564  infdifsn  9639  infdiffi  9640  isnum2  9953  wdomfil  10067  djuen  10175  djuenun  10176  djudom2  10189  djuxpdom  10191  djuinf  10194  infdju1  10195  pwdjuidm  10197  djulepw  10198  infdjuabs  10210  infdif  10213  pwdjudom  10220  infpss  10221  infmap2  10222  fictb  10249  infpssALT  10318  enfin2i  10326  fin34  10395  fodomb  10532  wdomac  10533  iundom2g  10551  iundom  10553  sdomsdomcard  10571  infxpidm  10573  engch  10640  fpwwe2lem3  10645  canthp1lem1  10664  canthp1lem2  10665  canthp1  10666  pwfseq  10676  pwxpndom2  10677  pwxpndom  10678  pwdjundom  10679  hargch  10685  gchaclem  10690  hasheni  14415  hashdomi  14447  clim  15584  rlim  15585  ntrivcvgn0  15990  ssc1  17913  ssc2  17914  ssctr  17917  frgpnabl  20005  dprddomprc  20132  dprdval  20135  dprdgrp  20137  dprdf  20138  dprdssv  20148  subgdmdprd  20166  dprd2da  20174  1stcrestlem  23680  hauspwdom  23730  isref  23738  ufilen  24159  dvle  26237  ellpi  33810  finextfldext  34177  locfinref  34354  karddom  35690  kardsdom  35691  isfne4  36962  fnetr  36973  topfneec  36977  fnessref  36979  refssfne  36980  bj-epelb  37816  bj-idreseq  37917  phpreu  38361  sdomne0  44256  sdomne0d  44257  rn1st  46105  climf  46455  climf2  46497  iinfssc  49986  fuco21  50265  fucoid  50277