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 2146  Vcvv 3454   class class class wbr 5106  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662

This theorem is used by:  vtoclr  5718  brfvopabrbr  7001  domdifsn  9093  undom  9098  xpdom2  9105  xpdom1g  9107  domunsncan  9110  enfixsn  9119  fodomr  9161  pwdom  9162  domssex  9171  xpen  9173  mapdom1  9175  mapdom2  9181  pwen  9183  domtrfil  9221  sucdom2  9232  0sdom1dom  9251  1sdom2dom  9259  unxpdom  9264  unxpdom2  9265  sucxpdom  9266  isfinite2  9304  infn0ALT  9309  fin2inf  9310  fodomfir  9333  suppeqfsuppbi  9384  fsuppsssupp  9386  fsuppssov1  9389  fsuppunbi  9394  funsnfsupp  9397  mapfien2  9414  wemapso2  9560  card2on  9561  elharval  9568  harword  9570  brwdomi  9575  brwdomn0  9576  domwdom  9581  wdomtr  9582  wdompwdom  9585  canthwdom  9586  brwdom3i  9590  unwdomg  9591  xpwdomg  9592  unxpwdom  9596  infdifsn  9671  infdiffi  9672  isnum2  10039  wdomfil  10153  djuen  10261  djuenun  10262  djudom2  10275  djuxpdom  10277  djuinf  10280  infdju1  10281  pwdjuidm  10283  djulepw  10284  infdjuabs  10296  infdif  10299  pwdjudom  10306  infpss  10307  infmap2  10308  fictb  10335  infpssALT  10404  enfin2i  10412  fin34  10481  fodomb  10618  wdomac  10619  iundom2g  10637  iundom  10639  sdomsdomcard  10657  infxpidm  10659  engch  10726  fpwwe2lem3  10731  canthp1lem1  10750  canthp1lem2  10751  canthp1  10752  pwfseq  10762  pwxpndom2  10763  pwxpndom  10764  pwdjundom  10765  hargch  10771  gchaclem  10776  hasheni  14505  hashdomi  14537  clim  15676  rlim  15677  ntrivcvgn0  16082  ssc1  18011  ssc2  18012  ssctr  18015  frgpnabl  20104  dprddomprc  20231  dprdval  20234  dprdgrp  20236  dprdf  20237  dprdssv  20247  subgdmdprd  20265  dprd2da  20273  1stcrestlem  23785  hauspwdom  23835  isref  23843  ufilen  24264  dvle  26342  ellpi  33984  finextfldext  34352  locfinref  34529  weexenwe  35830  karddom  35903  kardsdom  35904  isfne4  37258  fnetr  37269  topfneec  37273  fnessref  37275  refssfne  37276  bj-epelb  38126  bj-idreseq  38226  phpreu  38670  sdomne0  44557  sdomne0d  44558  rn1st  46427  climf  46776  climf2  46818  iinfssc  50313  fuco21  50600  fucoid  50612