MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brrelex2i Structured version   Visualization version   GIF version

Theorem brrelex2i 5645
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
StepHypRef Expression
1 brrelexi.1 . 2 Rel 𝑅
2 brrelex2 5642 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
31, 2mpan 687 1 (𝐴𝑅𝐵𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3433   class class class wbr 5075  Rel wrel 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-xp 5596  df-rel 5597
This theorem is referenced by:  vtoclr  5651  brfvopabrbr  6881  brdomiOLD  8758  domdifsn  8850  undom  8855  undomOLD  8856  xpdom2  8863  xpdom1g  8865  domunsncan  8868  enfixsn  8877  sucdom2OLD  8878  fodomr  8924  pwdom  8925  domssex  8934  xpen  8936  mapdom1  8938  mapdom2  8944  pwen  8946  domtrfil  8987  sucdom2  8998  unxpdom  9039  unxpdom2  9040  sucxpdom  9041  isfinite2  9081  infn0  9085  fin2inf  9086  suppeqfsuppbi  9151  fsuppsssupp  9153  fsuppunbi  9158  funsnfsupp  9161  mapfien2  9177  wemapso2  9321  card2on  9322  elharval  9329  harword  9331  brwdomi  9336  brwdomn0  9337  domwdom  9342  wdomtr  9343  wdompwdom  9346  canthwdom  9347  brwdom3i  9351  unwdomg  9352  xpwdomg  9353  unxpwdom  9357  infdifsn  9424  infdiffi  9425  isnum2  9712  wdomfil  9826  djuen  9934  djuenun  9935  djudom2  9948  djuxpdom  9950  djuinf  9953  infdju1  9954  pwdjuidm  9956  djulepw  9957  infdjuabs  9971  infdif  9974  pwdjudom  9981  infpss  9982  infmap2  9983  fictb  10010  infpssALT  10078  enfin2i  10086  fin34  10155  fodomb  10291  wdomac  10292  iundom2g  10305  iundom  10307  sdomsdomcard  10325  infxpidm  10327  engch  10393  fpwwe2lem3  10398  canthp1lem1  10417  canthp1lem2  10418  canthp1  10419  pwfseq  10429  pwxpndom2  10430  pwxpndom  10431  pwdjundom  10432  hargch  10438  gchaclem  10443  hasheni  14071  hashdomi  14104  clim  15212  rlim  15213  ntrivcvgn0  15619  ssc1  17542  ssc2  17543  ssctr  17546  frgpnabl  19485  dprddomprc  19612  dprdval  19615  dprdgrp  19617  dprdf  19618  dprdssv  19628  subgdmdprd  19646  dprd2da  19654  1stcrestlem  22612  hauspwdom  22661  isref  22669  ufilen  23090  dvle  25180  locfinref  31800  isfne4  34538  fnetr  34549  topfneec  34553  fnessref  34555  refssfne  34556  bj-epelb  35249  bj-idreseq  35342  phpreu  35770  climf  43170  climf2  43214
  Copyright terms: Public domain W3C validator