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

Theorem brrelex2i 5046
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
Assertion
Ref Expression
brrelex2i

Proof of Theorem brrelex2i
StepHypRef Expression
1 brrelexi.1 . 2
2 brrelex2 5044 . 2
31, 2mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cvv 3109   class class class wbr 4452  Relwrel 5009
This theorem is referenced by:  vtoclr  5049  brdomi  7547  domdifsn  7620  undom  7625  xpdom2  7632  xpdom1g  7634  domunsncan  7637  enfixsn  7646  fodomr  7688  pwdom  7689  domssex  7698  xpen  7700  mapdom1  7702  mapdom2  7708  pwen  7710  sucdom2  7734  unxpdom  7747  unxpdom2  7748  sucxpdom  7749  isfinite2  7798  infn0  7802  fin2inf  7803  fsuppimp  7855  suppeqfsuppbi  7863  fsuppsssupp  7865  fsuppunbi  7870  funsnfsupp  7873  mapfien2  7888  wemapso2  8000  card2on  8001  elharval  8010  harword  8012  brwdomi  8015  brwdomn0  8016  domwdom  8021  wdomtr  8022  wdompwdom  8025  canthwdom  8026  brwdom3i  8030  unwdomg  8031  xpwdomg  8032  unxpwdom  8036  infdifsn  8094  infdiffi  8095  isnum2  8347  wdomfil  8463  cdaen  8574  cdaenun  8575  cdadom1  8587  cdaxpdom  8590  cdainf  8593  infcda1  8594  pwcdaidm  8596  cdalepw  8597  infpss  8618  infmap2  8619  fictb  8646  infpssALT  8714  enfin2i  8722  fin34  8791  fodomb  8925  wdomac  8926  iundom2g  8936  iundom  8938  sdomsdomcard  8956  infxpidm  8958  engch  9027  fpwwe2lem3  9032  canthp1lem1  9051  canthp1lem2  9052  canthp1  9053  pwfseq  9063  pwxpndom2  9064  pwxpndom  9065  pwcdandom  9066  hargch  9072  gchaclem  9077  hasheni  12421  hashdomi  12448  brfi1uzind  12532  clim  13317  rlim  13318  ntrivcvgn0  13707  ssc1  15190  ssc2  15191  ssctr  15194  frgpnabl  16879  dprddomprc  17031  dprdval  17034  dprdvalOLD  17036  dprdgrp  17038  dprdf  17039  dprdwOLD  17050  dprdssv  17056  dprdfidOLD  17064  dprdfinvOLD  17066  dprdfaddOLD  17067  dprdfsubOLD  17068  dprdfeq0OLD  17069  dprdf11OLD  17070  subgdmdprd  17081  dmdprdsplitlemOLD  17085  dprddisj2OLD  17088  dprd2da  17091  dpjidclOLD  17114  1stcrestlem  19953  hauspwdom  20002  isref  20010  ufilen  20431  dvle  22408  uhgrav  24296  ushgraf  24302  ushgrauhgra  24303  umgraf2  24317  umgrares  24324  umisuhgra  24327  umgraun  24328  uslgrav  24337  usgrav  24338  uslgraf  24345  iscusgra0  24457  frisusgrapr  24991  locfinref  27844  isfne4  30158  fnetr  30169  topfneec  30173  fnessref  30175  refssfne  30176  mapfien2OLD  31042  climf  31628  linindsv  33046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011
  Copyright terms: Public domain W3C validator