Theorem breq2 4134

Description: Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
breq2	|- ( A = B -> ( C R A <-> C R B ) )

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3905	. . 3 |- ( A = B -> <. C , A >. = <. C , B >. )
2	1	eleq1d 2307	. 2 |- ( A = B -> ( <. C , A >. e. R <-> <. C , B >. e. R ) )
3		df-br 4131	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4131	. 2 |- ( C R B <-> <. C , B >. e. R )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( C R A <-> C R B ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209   <.cop 3712   class class class wbr 4130

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-br 4131

This theorem is used by:  breq12  4135  breq2i  4138  breq2d  4142  nbrne1  4149  brralrspcev  4189  brimralrspcev  4190  pocl  4448  swopolem  4450  swopo  4451  sowlin  4465  sotricim  4468  sotritrieq  4470  seex  4480  frind  4497  wetriext  4724  vtoclr  4823  posng  4847  brcog  4947  brcogw  4949  opelcnvg  4960  dfdmf  4974  breldmg  4987  dfrnf  5023  dmcoss  5052  resieq  5073  dfres2  5115  elimag  5130  elrelimasn  5153  elimasn  5154  intirr  5174  poirr2  5180  poltletr  5188  dffun6f  5390  dffun4f  5393  fun11  5448  brprcneu  5688  fv3  5718  tz6.12c  5725  relelfvdm  5727  fvmbr  5731  funbrfv  5739  fnbrfvb  5741  funfvdm2f  5768  fndmdif  5814  dff3im  5853  fmptco  5874  foeqcnvco  5996  isorel  6014  isocnv  6017  isotr  6022  isopolem  6028  isosolem  6030  f1oiso  6032  f1oiso2  6033  caovordig  6255  caovordg  6257  caovord  6261  caofrss  6334  caoftrn  6335  poxp  6468  tposoprab  6551  ertr  6822  ecopovsym  6905  ecopovtrn  6906  ecopovsymg  6908  ecopovtrng  6909  th3qlem2  6912  domeng  7036  eqeng  7052  snfig  7103  nneneq  7158  nnfi  7174  ssfilem  7177  ssfilemd  7179  domfiexmid  7182  dif1enen  7184  diffitest  7191  findcard  7192  findcard2  7193  findcard2s  7194  diffisn  7197  tridc  7204  fimax2gtrilemstep  7205  inffiexmid  7213  unsnfi  7226  fiintim  7238  fisseneq  7242  isbth  7284  supmoti  7333  eqsupti  7336  supubti  7339  suplubti  7340  suplub2ti  7341  supmaxti  7344  supsnti  7345  isotilem  7346  isoti  7347  supisolem  7348  supisoex  7349  cardcl  7526  isnumi  7527  cardval3ex  7530  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  papsym  7612  papcotr  7613  exmidapne  7626  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  nsmallnqq  7779  subhalfnqq  7781  ltbtwnnqq  7782  prarloclemarch2  7786  nqnq0pi  7805  prcdnql  7851  prcunqu  7852  prnminu  7856  genpcdl  7886  genprndl  7888  genprndu  7889  genpdisj  7890  nqprm  7909  nqprrnd  7910  nqprdisj  7911  nqprloc  7912  nqprlu  7914  nqprl  7918  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  1idpru  7958  ltnqpr  7960  ltnqpri  7961  prplnqu  7987  recexprlemelu  7990  recexprlemm  7991  recexprlemloc  7998  recexprlem1ssl  8000  recexprlemss1u  8003  cauappcvgprlemm  8012  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem2  8047  caucvgprprlemelu  8053  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexpr  8092  lttrsr  8129  ltsosr  8131  ltasrg  8137  recexgt0sr  8140  mulgt0sr  8145  aptisr  8146  mulextsr1  8148  srpospr  8150  caucvgsrlemgt1  8162  caucvgsrlemoffres  8167  caucvgsr  8169  map2psrprg  8172  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  axprecex  8247  axpre-ltwlin  8250  axpre-lttrn  8251  axpre-apti  8252  axpre-ltadd  8253  axpre-mulgt0  8254  axpre-mulext  8255  axcaucvglemcau  8265  axcaucvglemres  8266  axcaucvg  8267  axpre-suploclemres  8268  axpre-suploc  8269  ltxrlt  8391  lttri3  8405  ltne  8410  eqle  8417  ltordlem  8810  reapti  8907  apreim  8931  squeeze0  9234  lbreu  9275  lble  9277  suprleubex  9284  sup3exmid  9287  nnge1  9327  nn2ge  9337  nn1gt1  9338  nnsub  9343  nominpos  9543  nn0ge0  9588  elnnnn0b  9607  nn0ge2m1nn  9627  zdclt  9722  suprzclex  9744  peano2uz2  9753  peano5uzti  9754  dfuzi  9756  uzind  9757  uzind3  9759  eluz1  9925  uzind4  9988  indstr  9993  supinfneg  9995  infsupneg  9996  infregelbex  9998  indstr2  10009  ublbneg  10013  irrmulap  10048  elpq  10049  elpqb  10050  elrp  10056  mnfltxr  10188  nn0pnfge0  10193  xrltnsym  10195  xrlttr  10197  xrltso  10198  xrlttri3  10199  xrltne  10215  ngtmnft  10219  nmnfgt  10220  xrrebnd  10221  z2ge  10228  xltnegi  10237  xltadd1  10278  xsubge0  10283  xleaddadd  10289  ixxval  10298  elixx1  10299  elioo2  10323  iccid  10327  iccsupr  10368  repos  10372  fzval  10413  elfz1  10416  fzm1  10507  zsupcllemstep  10662  suprzubdc  10671  zsupssdc  10673  qdclt  10680  exbtwnzlemstep  10682  exbtwnzlemex  10684  qbtwnre  10691  qbtwnxr  10692  flval  10707  apbtwnz  10709  modqid2  10788  modqmuladdnn0  10805  exp3val  10978  expge0  11012  expge1  11013  nn0ltexp2  11147  facdiv  11176  facwordi  11178  hashinfom  11217  hashennn  11219  hashunlem  11244  zfz1iso  11293  wrdlen1  11342  fstwrdne0  11344  wrdl1exs1  11397  pfxsuffeqwrdeq  11470  pfxsuff1eqwrdeq  11471  ccats1pfxeq  11486  ccats1pfxeqrex  11487  pfxccatin12lem3  11504  ovshftex  11584  shftfibg  11585  shftfib  11588  shftfn  11589  2shfti  11596  sqrt0rlem  11769  resqrexlemex  11791  rsqrmo  11793  resqrtcl  11795  rersqrtthlem  11796  sqrtsq  11810  cau3lem  11880  caubnd2  11883  maxleim  11971  maxabslemval  11974  maxleast  11979  maxleb  11982  fimaxre2  11993  minmax  11996  xrmaxleim  12010  xrmaxiflemval  12016  xrmaxaddlem  12026  xrminmax  12031  xrbdtri  12042  climi  12053  climeu  12062  climmo  12064  2clim  12067  addcn2  12076  mulcn2  12078  reccn2ap  12079  cn1lem  12080  summodc  12150  zsumdc  12151  fsum3  12154  cvgratz  12299  ntrivcvgap0  12316  prodmodc  12345  zproddc  12346  fprodseq  12350  fprodntrivap  12351  sinltxirr  12528  dvdsabsb  12577  0dvds  12578  alzdvds  12621  dvdsext  12622  fzo0dvdseq  12624  2tp1odd  12651  2teven  12654  divalglemnn  12685  divalglemeunn  12688  divalglemeuneg  12690  bitsinv1lem  12728  gcdval  12736  gcddvds  12740  bezoutlemstep  12774  bezoutlemmain  12775  bezoutlemex  12778  bezoutlemeu  12784  bezoutlemsup  12786  dfgcd3  12787  bezout  12788  dvdsgcd  12789  dfgcd2  12791  dvdssq  12808  uzwodc  12814  nnwofdc  12815  lcmval  12841  lcmcllem  12845  dvdslcm  12847  lcmledvds  12848  lcmgcdlem  12855  lcmdvds  12857  coprmgcdb  12866  coprmdvds2  12871  cncongr1  12881  cncongr2  12882  isprm  12887  dvdsnprmd  12903  dvdsprm  12915  exprmfct  12916  isprm6  12925  prmexpb  12929  prmfac1  12930  rpexp  12931  sqrt2irr  12940  oddpwdclemdc  12951  oddpwdc  12952  sqpweven  12953  2sqpwodd  12954  sqne2sq  12955  nnoddn2prmb  13041  pceu  13074  pczpre  13076  pcdiv  13081  pcdvdsb  13099  difsqpwdvds  13117  pcmpt  13122  pcmptdvds  13124  oddprmdvds  13133  prmpwdvds  13134  infpnlem2  13139  ballotfilemfcc  13233  oddennn  13283  evenennn  13284  exmidunben  13317  nninfdclemcl  13339  nninfdclemp1  13341  nninfdc  13344  infpn2  13347  eqgen  14030  zndvds  14984  znleval  14988  comet  15600  metcnpi  15616  metcnpi2  15617  metcnpi3  15618  addcncntoplem  15662  cncfi  15679  elcncf1di  15680  mulcncflem  15708  dedekindeulemuub  15718  dedekindeulemloc  15720  dedekindeulemlu  15722  dedekindeulemeu  15723  dedekindeu  15724  suplociccreex  15725  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemloc  15729  dedekindicclemlu  15731  dedekindicclemeu  15732  dedekindicclemicc  15733  dedekindicc  15734  ivthinclemlopn  15737  ivthinclemlr  15738  ivthinclemuopn  15739  ivthinclemur  15740  ivthinclemloc  15742  ivthinc  15744  ivthreinc  15746  dich0  15753  ivthdich  15754  limcimo  15766  cnplimclemr  15770  limccnp2lem  15777  limccoap  15779  eldvap  15783  logltb  15975  pellexlem3  16093  lgsdir  16154  lgsne0  16157  gausslemma2dlem0i  16176  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  2lgslem2  16211  2lgs  16223  2sqlem6  16239  2sqlem8  16242  2sqlem10  16244  lfgredg2dom  16373  istrl  16626  clwwlkn0  16649  clwwlkext2edg  16663  clwwlknonccat  16674  clwwlknonex2  16680  iseupth  16688  konigsberg  16734  lealltlt2  16752  sbthom  17071  trilpo  17092  trirec0  17093  apdiff  17097  reap0  17108  cndcap  17109  nconstwlpolem  17115  neapmkv  17118  neap0mkv  17119  ltlenmkv  17120