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

Theorem brrelex2i 5193
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 5191 . 2 ((Rel 𝑅𝐴𝑅𝐵) → 𝐵 ∈ V)
31, 2mpan 706 1 (𝐴𝑅𝐵𝐵 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  Vcvv 3231   class class class wbr 4685  Rel wrel 5148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-rel 5150
This theorem is referenced by:  vtoclr  5198  brfvopabrbr  6318  brdomi  8008  domdifsn  8084  undom  8089  xpdom2  8096  xpdom1g  8098  domunsncan  8101  enfixsn  8110  fodomr  8152  pwdom  8153  domssex  8162  xpen  8164  mapdom1  8166  mapdom2  8172  pwen  8174  sucdom2  8197  unxpdom  8208  unxpdom2  8209  sucxpdom  8210  isfinite2  8259  infn0  8263  fin2inf  8264  fsuppimp  8322  suppeqfsuppbi  8330  fsuppsssupp  8332  fsuppunbi  8337  funsnfsupp  8340  mapfien2  8355  wemapso2  8499  card2on  8500  elharval  8509  harword  8511  brwdomi  8514  brwdomn0  8515  domwdom  8520  wdomtr  8521  wdompwdom  8524  canthwdom  8525  brwdom3i  8529  unwdomg  8530  xpwdomg  8531  unxpwdom  8535  infdifsn  8592  infdiffi  8593  isnum2  8809  wdomfil  8922  cdaen  9033  cdaenun  9034  cdadom1  9046  cdaxpdom  9049  cdainf  9052  infcda1  9053  pwcdaidm  9055  cdalepw  9056  infpss  9077  infmap2  9078  fictb  9105  infpssALT  9173  enfin2i  9181  fin34  9250  fodomb  9386  wdomac  9387  iundom2g  9400  iundom  9402  sdomsdomcard  9420  infxpidm  9422  engch  9488  fpwwe2lem3  9493  canthp1lem1  9512  canthp1lem2  9513  canthp1  9514  pwfseq  9524  pwxpndom2  9525  pwxpndom  9526  pwcdandom  9527  hargch  9533  gchaclem  9538  hasheni  13176  hashdomi  13207  brfi1indALT  13320  clim  14269  rlim  14270  ntrivcvgn0  14674  ssc1  16528  ssc2  16529  ssctr  16532  frgpnabl  18324  dprddomprc  18445  dprdval  18448  dprdgrp  18450  dprdf  18451  dprdssv  18461  subgdmdprd  18479  dprd2da  18487  1stcrestlem  21303  hauspwdom  21352  isref  21360  ufilen  21781  dvle  23815  subgrv  26207  locfinref  30036  isfne4  32460  fnetr  32471  topfneec  32475  fnessref  32477  refssfne  32478  phpreu  33523  climf  40172  climf2  40216  linindsv  42559
  Copyright terms: Public domain W3C validator