ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  breq2 GIF version

Theorem breq2 3826
Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
breq2 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))

Proof of Theorem breq2
StepHypRef Expression
1 opeq2 3608 . . 3 (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
21eleq1d 2153 . 2 (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3 df-br 3823 . 2 (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4 df-br 3823 . 2 (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
52, 3, 43bitr4g 221 1 (𝐴 = 𝐵 → (𝐶𝑅𝐴𝐶𝑅𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = wceq 1287  wcel 1436  cop 3434   class class class wbr 3822
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-un 2992  df-sn 3437  df-pr 3438  df-op 3440  df-br 3823
This theorem is referenced by:  breq12  3827  breq2i  3830  breq2d  3834  nbrne1  3839  pocl  4106  swopolem  4108  swopo  4109  sowlin  4123  sotricim  4126  sotritrieq  4128  seex  4138  frind  4155  wetriext  4367  vtoclr  4456  posng  4480  brcog  4573  brcogw  4575  opelcnvg  4586  dfdmf  4599  breldmg  4612  dfrnf  4646  dmcoss  4672  resieq  4693  dfres2  4733  elimag  4747  elreimasng  4767  elimasn  4768  intirr  4787  poirr2  4793  poltletr  4801  dffun6f  4996  dffun4f  4999  fun11  5048  brprcneu  5263  fv3  5293  tz6.12c  5299  relelfvdm  5301  funbrfv  5308  fnbrfvb  5310  funfvdm2f  5334  fndmdif  5369  dff3im  5409  fmptco  5429  foeqcnvco  5532  isorel  5550  isocnv  5553  isotr  5558  isopolem  5564  isosolem  5566  f1oiso  5568  f1oiso2  5569  caovordig  5769  caovordg  5771  caovord  5775  caofrss  5838  caoftrn  5839  poxp  5956  tposoprab  6001  ertr  6261  ecopovsym  6342  ecopovtrn  6343  ecopovsymg  6345  ecopovtrng  6346  th3qlem2  6349  domeng  6423  eqeng  6437  snfig  6485  nneneq  6527  nnfi  6542  ssfilem  6545  domfiexmid  6548  dif1enen  6550  diffitest  6557  findcard  6558  findcard2  6559  findcard2s  6560  diffisn  6563  tridc  6569  fimax2gtrilemstep  6570  inffiexmid  6576  unsnfi  6583  fisseneq  6595  isbth  6623  supmoti  6635  eqsupti  6638  supubti  6641  suplubti  6642  suplub2ti  6643  supmaxti  6646  supsnti  6647  isotilem  6648  isoti  6649  supisolem  6650  supisoex  6651  cardcl  6756  isnumi  6757  cardval3ex  6760  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  nqtri3or  6902  ltsonq  6904  ltanqg  6906  ltmnqg  6907  ltexnqq  6914  nsmallnqq  6918  subhalfnqq  6920  ltbtwnnqq  6921  prarloclemarch2  6925  nqnq0pi  6944  prcdnql  6990  prcunqu  6991  prnminu  6995  genpcdl  7025  genprndl  7027  genprndu  7028  genpdisj  7029  nqprm  7048  nqprrnd  7049  nqprdisj  7050  nqprloc  7051  nqprlu  7053  nqprl  7057  addnqprlemru  7064  addnqprlemfl  7065  addnqprlemfu  7066  mulnqprlemru  7080  mulnqprlemfl  7081  mulnqprlemfu  7082  1idpru  7097  ltnqpr  7099  ltnqpri  7100  prplnqu  7126  recexprlemelu  7129  recexprlemm  7130  recexprlemloc  7137  recexprlem1ssl  7139  recexprlemss1u  7142  cauappcvgprlemm  7151  cauappcvgprlemopu  7154  cauappcvgprlemupu  7155  cauappcvgprlemdisj  7157  cauappcvgprlemloc  7158  cauappcvgprlemladdfu  7160  cauappcvgprlemladdru  7162  cauappcvgprlemladdrl  7163  cauappcvgprlem2  7166  caucvgprlemnkj  7172  caucvgprlemnbj  7173  caucvgprlemm  7174  caucvgprlemopu  7177  caucvgprlemupu  7178  caucvgprlemdisj  7180  caucvgprlemloc  7181  caucvgprlemcl  7182  caucvgprlemladdfu  7183  caucvgprlemladdrl  7184  caucvgprlem2  7186  caucvgprprlemelu  7192  caucvgprprlemcbv  7193  caucvgprprlemval  7194  caucvgprprlemnbj  7199  caucvgprprlemmu  7201  caucvgprprlemexbt  7212  caucvgprprlemaddq  7214  caucvgprprlem1  7215  caucvgprprlem2  7216  lttrsr  7255  ltsosr  7257  ltasrg  7263  recexgt0sr  7266  mulgt0sr  7270  aptisr  7271  mulextsr1  7273  srpospr  7275  caucvgsrlemgt1  7287  caucvgsrlemoffres  7292  caucvgsr  7294  axprecex  7362  axpre-ltwlin  7365  axpre-lttrn  7366  axpre-apti  7367  axpre-ltadd  7368  axpre-mulgt0  7369  axpre-mulext  7370  axcaucvglemcau  7380  axcaucvglemres  7381  axcaucvg  7382  ltxrlt  7499  lttri3  7512  ltne  7517  eqle  7523  reapti  8000  apreim  8024  squeeze0  8303  lbreu  8344  lble  8346  suprleubex  8353  nnge1  8383  nn2ge  8392  nn1gt1  8393  nnsub  8398  nominpos  8589  nn0ge0  8634  elnnnn0b  8653  nn0ge2m1nn  8669  zdclt  8760  suprzclex  8780  peano2uz2  8789  peano5uzti  8790  dfuzi  8792  uzind  8793  uzind3  8795  eluz1  8958  uzind4  9011  indstr  9016  supinfneg  9018  infsupneg  9019  indstr2  9031  ublbneg  9033  elrp  9071  mnfltxr  9191  nn0pnfge0  9196  xrltnsym  9198  xrlttr  9200  xrltso  9201  xrlttri3  9202  xrltne  9213  ngtmnft  9215  xrrebnd  9216  z2ge  9223  xltnegi  9232  ixxval  9249  elixx1  9250  elioo2  9274  iccid  9278  iccsupr  9319  repos  9323  fzval  9361  elfz1  9364  fzm1  9447  exbtwnzlemstep  9590  exbtwnzlemex  9592  qbtwnre  9599  qbtwnxr  9600  flval  9610  apbtwnz  9612  modqid2  9689  modqmuladdnn0  9706  serige0  9854  expival  9859  expge0  9893  expge1  9894  facdiv  10046  facwordi  10048  hashinfom  10086  hashennn  10088  hashunlem  10112  zfz1iso  10146  ovshftex  10153  shftfibg  10154  shftfib  10157  shftfn  10158  2shfti  10165  sqrt0rlem  10335  resqrexlemex  10357  rsqrmo  10359  resqrtcl  10361  rersqrtthlem  10362  sqrtsq  10376  cau3lem  10446  caubnd2  10449  maxleim  10537  maxabslemval  10540  maxleast  10545  maxleb  10548  fimaxre2  10556  minmax  10559  climi  10573  climeu  10582  climmo  10584  2clim  10587  addcn2  10596  mulcn2  10598  cn1lem  10599  isummo  10667  zisum  10668  fisum  10670  dvdsabsb  10721  0dvds  10722  alzdvds  10761  dvdsext  10762  fzo0dvdseq  10764  2tp1odd  10790  2teven  10793  divalglemnn  10824  divalglemeunn  10827  divalglemeuneg  10829  zsupcllemstep  10847  gcdval  10857  gcddvds  10861  bezoutlemstep  10892  bezoutlemmain  10893  bezoutlemex  10896  bezoutlemeu  10902  bezoutlemsup  10904  dfgcd3  10905  bezout  10906  dvdsgcd  10907  dfgcd2  10909  dvdssq  10926  lcmval  10951  lcmcllem  10955  dvdslcm  10957  lcmledvds  10958  lcmgcdlem  10965  lcmdvds  10967  coprmgcdb  10976  coprmdvds2  10981  cncongr1  10991  cncongr2  10992  isprm  10997  dvdsnprmd  11013  dvdsprm  11024  exprmfct  11025  isprm6  11032  prmexpb  11036  prmfac1  11037  rpexp  11038  sqrt2irr  11047  oddpwdclemdc  11057  oddpwdc  11058  sqpweven  11059  2sqpwodd  11060  sqne2sq  11061  oddennn  11111  evenennn  11112
  Copyright terms: Public domain W3C validator