Theorem brrelex2i 5708

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

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

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 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-rel 5658

This theorem is used by:  vtoclr  5714  brfvopabrbr  6990  domdifsn  9079  undom  9084  xpdom2  9091  xpdom1g  9093  domunsncan  9096  enfixsn  9105  fodomr  9147  pwdom  9148  domssex  9157  xpen  9159  mapdom1  9161  mapdom2  9167  pwen  9169  domtrfil  9207  sucdom2  9218  0sdom1dom  9237  1sdom2dom  9245  unxpdom  9250  unxpdom2  9251  sucxpdom  9252  isfinite2  9290  infn0ALT  9295  fin2inf  9296  fodomfir  9319  suppeqfsuppbi  9371  fsuppsssupp  9373  fsuppssov1  9376  fsuppunbi  9381  funsnfsupp  9384  mapfien2  9401  wemapso2  9547  card2on  9548  elharval  9555  harword  9557  brwdomi  9562  brwdomn0  9563  domwdom  9568  wdomtr  9569  wdompwdom  9572  canthwdom  9573  brwdom3i  9577  unwdomg  9578  xpwdomg  9579  unxpwdom  9583  infdifsn  9658  infdiffi  9659  isnum2  10026  wdomfil  10140  djuen  10248  djuenun  10249  djudom2  10262  djuxpdom  10264  djuinf  10267  infdju1  10268  pwdjuidm  10270  djulepw  10271  infdjuabs  10283  infdif  10286  pwdjudom  10293  infpss  10294  infmap2  10295  fictb  10322  infpssALT  10391  enfin2i  10399  fin34  10468  fodomb  10605  wdomac  10606  iundom2g  10624  iundom  10626  sdomsdomcard  10644  infxpidm  10646  engch  10713  fpwwe2lem3  10718  canthp1lem1  10737  canthp1lem2  10738  canthp1  10739  pwfseq  10749  pwxpndom2  10750  pwxpndom  10751  pwdjundom  10752  hargch  10758  gchaclem  10763  hasheni  14492  hashdomi  14524  clim  15661  rlim  15662  ntrivcvgn0  16067  ssc1  17996  ssc2  17997  ssctr  18000  frgpnabl  20089  dprddomprc  20216  dprdval  20219  dprdgrp  20221  dprdf  20222  dprdssv  20232  subgdmdprd  20250  dprd2da  20258  1stcrestlem  23770  hauspwdom  23820  isref  23828  ufilen  24249  dvle  26327  ellpi  33928  finextfldext  34296  locfinref  34473  weexenwe  35756  karddom  35829  kardsdom  35830  isfne4  37128  fnetr  37139  topfneec  37143  fnessref  37145  refssfne  37146  bj-epelb  37984  bj-idreseq  38083  phpreu  38527  sdomne0  44413  sdomne0d  44414  rn1st  46284  climf  46633  climf2  46675  iinfssc  50164  fuco21  50443  fucoid  50455