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

Theorem brrelex2i 5577
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 5574 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
31, 2mpan 689 1 (𝐴𝑅𝐵𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3444   class class class wbr 5033  Rel wrel 5528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-rel 5530
This theorem is referenced by:  vtoclr  5583  brfvopabrbr  6746  brdomi  8507  domdifsn  8587  undom  8592  xpdom2  8599  xpdom1g  8601  domunsncan  8604  enfixsn  8613  sucdom2  8614  fodomr  8656  pwdom  8657  domssex  8666  xpen  8668  mapdom1  8670  mapdom2  8676  pwen  8678  unxpdom  8713  unxpdom2  8714  sucxpdom  8715  isfinite2  8764  infn0  8768  fin2inf  8769  suppeqfsuppbi  8835  fsuppsssupp  8837  fsuppunbi  8842  funsnfsupp  8845  mapfien2  8860  wemapso2  9005  card2on  9006  elharval  9013  harword  9015  brwdomi  9020  brwdomn0  9021  domwdom  9026  wdomtr  9027  wdompwdom  9030  canthwdom  9031  brwdom3i  9035  unwdomg  9036  xpwdomg  9037  unxpwdom  9041  infdifsn  9108  infdiffi  9109  isnum2  9362  wdomfil  9476  djuen  9584  djuenun  9585  djudom2  9598  djuxpdom  9600  djuinf  9603  infdju1  9604  pwdjuidm  9606  djulepw  9607  infdjuabs  9621  infdif  9624  pwdjudom  9631  infpss  9632  infmap2  9633  fictb  9660  infpssALT  9728  enfin2i  9736  fin34  9805  fodomb  9941  wdomac  9942  iundom2g  9955  iundom  9957  sdomsdomcard  9975  infxpidm  9977  engch  10043  fpwwe2lem3  10048  canthp1lem1  10067  canthp1lem2  10068  canthp1  10069  pwfseq  10079  pwxpndom2  10080  pwxpndom  10081  pwdjundom  10082  hargch  10088  gchaclem  10093  hasheni  13708  hashdomi  13741  clim  14846  rlim  14847  ntrivcvgn0  15249  ssc1  17086  ssc2  17087  ssctr  17090  frgpnabl  18991  dprddomprc  19118  dprdval  19121  dprdgrp  19123  dprdf  19124  dprdssv  19134  subgdmdprd  19152  dprd2da  19160  1stcrestlem  22060  hauspwdom  22109  isref  22117  ufilen  22538  dvle  24613  locfinref  31194  isfne4  33796  fnetr  33807  topfneec  33811  fnessref  33813  refssfne  33814  bj-epelb  34480  bj-idreseq  34572  phpreu  35034  climf  42251  climf2  42295
  Copyright terms: Public domain W3C validator