Theorem brrelex2i 5720

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457   class class class wbr 5111  Rel wrel 5668

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-rel 5670

This theorem is used by:  vtoclr  5726  brfvopabrbr  6990  domdifsn  9055  undom  9060  xpdom2  9067  xpdom1g  9069  domunsncan  9072  enfixsn  9081  fodomr  9123  pwdom  9124  domssex  9133  xpen  9135  mapdom1  9137  mapdom2  9143  pwen  9145  domtrfil  9183  sucdom2  9194  0sdom1dom  9213  1sdom2dom  9221  unxpdom  9226  unxpdom2  9227  sucxpdom  9228  isfinite2  9265  infn0ALT  9270  fin2inf  9271  fodomfir  9294  suppeqfsuppbi  9346  fsuppsssupp  9348  fsuppssov1  9351  fsuppunbi  9356  funsnfsupp  9359  mapfien2  9376  wemapso2  9522  card2on  9523  elharval  9530  harword  9532  brwdomi  9537  brwdomn0  9538  domwdom  9543  wdomtr  9544  wdompwdom  9547  canthwdom  9548  brwdom3i  9552  unwdomg  9553  xpwdomg  9554  unxpwdom  9558  infdifsn  9633  infdiffi  9634  isnum2  9947  wdomfil  10061  djuen  10169  djuenun  10170  djudom2  10183  djuxpdom  10185  djuinf  10188  infdju1  10189  pwdjuidm  10191  djulepw  10192  infdjuabs  10204  infdif  10207  pwdjudom  10214  infpss  10215  infmap2  10216  fictb  10243  infpssALT  10312  enfin2i  10320  fin34  10389  fodomb  10525  wdomac  10526  iundom2g  10541  iundom  10543  sdomsdomcard  10561  infxpidm  10563  engch  10630  fpwwe2lem3  10635  canthp1lem1  10654  canthp1lem2  10655  canthp1  10656  pwfseq  10666  pwxpndom2  10667  pwxpndom  10668  pwdjundom  10669  hargch  10675  gchaclem  10680  hasheni  14404  hashdomi  14436  clim  15571  rlim  15572  ntrivcvgn0  15977  ssc1  17902  ssc2  17903  ssctr  17906  frgpnabl  19991  dprddomprc  20118  dprdval  20121  dprdgrp  20123  dprdf  20124  dprdssv  20134  subgdmdprd  20152  dprd2da  20160  1stcrestlem  23661  hauspwdom  23711  isref  23719  ufilen  24140  dvle  26219  ellpi  33753  finextfldext  34120  locfinref  34297  karddom  35633  kardsdom  35634  isfne4  36910  fnetr  36921  topfneec  36925  fnessref  36927  refssfne  36928  bj-epelb  37764  bj-idreseq  37865  phpreu  38314  sdomne0  44199  sdomne0d  44200  rn1st  46048  climf  46398  climf2  46440  iinfssc  49894  fuco21  50173  fucoid  50185