Theorem breq2 4135

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 4132	. 2 |- ( C R A <-> <. C , A >. e. R )
4		df-br 4132	. 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 4131

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 4132

This theorem is used by:  breq12  4136  breq2i  4139  breq2d  4143  nbrne1  4150  brralrspcev  4190  brimralrspcev  4191  pocl  4450  swopolem  4452  swopo  4453  sowlin  4467  sotricim  4470  sotritrieq  4472  seex  4482  frind  4499  wetriext  4726  vtoclr  4825  posng  4849  brcog  4949  brcogw  4951  opelcnvg  4962  dfdmf  4976  breldmg  4989  dfrnf  5025  dmcoss  5054  resieq  5075  dfres2  5118  elimag  5133  elrelimasn  5156  elimasn  5157  intirr  5177  poirr2  5183  poltletr  5191  dffun6f  5393  dffun4f  5396  fun11  5451  brprcneu  5691  fv3  5721  tz6.12c  5728  relelfvdm  5730  fvmbr  5734  funbrfv  5742  fnbrfvb  5744  funfvdm2f  5771  fndmdif  5817  dff3im  5856  fmptco  5877  foeqcnvco  5999  isorel  6017  isocnv  6020  isotr  6025  isopolem  6031  isosolem  6033  f1oiso  6035  f1oiso2  6036  caovordig  6258  caovordg  6260  caovord  6264  caofrss  6338  caoftrn  6339  poxp  6472  tposoprab  6556  ertr  6827  ecopovsym  6910  ecopovtrn  6911  ecopovsymg  6913  ecopovtrng  6914  th3qlem2  6917  domeng  7042  eqeng  7058  snfig  7109  nneneq  7164  nnfi  7180  ssfilem  7183  ssfilemd  7185  domfiexmid  7188  dif1enen  7190  diffitest  7197  findcard  7198  findcard2  7199  findcard2s  7200  diffisn  7203  tridc  7210  fimax2gtrilemstep  7211  inffiexmid  7219  unsnfi  7232  fiintim  7244  fisseneq  7248  isbth  7291  supmoti  7339  eqsupti  7342  supubti  7345  suplubti  7346  suplub2ti  7347  supmaxti  7350  supsnti  7351  isotilem  7352  isoti  7353  supisolem  7354  supisoex  7355  cardcl  7532  isnumi  7533  cardval3ex  7536  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  papsym  7618  papcotr  7619  exmidapne  7632  nqtri3or  7769  ltsonq  7771  ltanqg  7773  ltmnqg  7774  ltexnqq  7781  nsmallnqq  7785  subhalfnqq  7787  ltbtwnnqq  7788  prarloclemarch2  7792  nqnq0pi  7811  prcdnql  7857  prcunqu  7858  prnminu  7862  genpcdl  7892  genprndl  7894  genprndu  7895  genpdisj  7896  nqprm  7915  nqprrnd  7916  nqprdisj  7917  nqprloc  7918  nqprlu  7920  nqprl  7924  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  1idpru  7964  ltnqpr  7966  ltnqpri  7967  prplnqu  7993  recexprlemelu  7996  recexprlemm  7997  recexprlemloc  8004  recexprlem1ssl  8006  recexprlemss1u  8009  cauappcvgprlemm  8018  cauappcvgprlemopu  8021  cauappcvgprlemupu  8022  cauappcvgprlemdisj  8024  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  cauappcvgprlem2  8033  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopu  8044  caucvgprlemupu  8045  caucvgprlemdisj  8047  caucvgprlemloc  8048  caucvgprlemcl  8049  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprlem2  8053  caucvgprprlemelu  8059  caucvgprprlemcbv  8060  caucvgprprlemval  8061  caucvgprprlemnbj  8066  caucvgprprlemmu  8068  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlem1  8082  caucvgprprlem2  8083  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemloc  8094  suplocexprlemub  8096  suplocexpr  8098  lttrsr  8135  ltsosr  8137  ltasrg  8143  recexgt0sr  8146  mulgt0sr  8151  aptisr  8152  mulextsr1  8154  srpospr  8156  caucvgsrlemgt1  8168  caucvgsrlemoffres  8173  caucvgsr  8175  map2psrprg  8178  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  axprecex  8253  axpre-ltwlin  8256  axpre-lttrn  8257  axpre-apti  8258  axpre-ltadd  8259  axpre-mulgt0  8260  axpre-mulext  8261  axcaucvglemcau  8271  axcaucvglemres  8272  axcaucvg  8273  axpre-suploclemres  8274  axpre-suploc  8275  ltxrlt  8397  lttri3  8411  ltne  8416  eqle  8423  ltordlem  8817  reapti  8915  apreim  8939  squeeze0  9242  lbreu  9283  lble  9285  suprleubex  9292  sup3exmid  9295  nnge1  9336  nn2ge  9346  nn1gt1  9347  nnsub  9352  nominpos  9554  nn0ge0  9599  elnnnn0b  9618  nn0ge2m1nn  9636  zdclt  9731  suprzclex  9754  peano2uz2  9763  peano5uzti  9764  dfuzi  9766  uzind  9767  uzind3  9769  eluz1  9940  uzind4  10003  indstr  10008  supinfneg  10010  infsupneg  10011  infregelbex  10013  indstr2  10024  ublbneg  10028  irraddap  10062  irrmulap  10064  elpq  10065  elpqb  10066  elrp  10072  mnfltxr  10204  nn0pnfge0  10209  xrltnsym  10211  xrlttr  10213  xrltso  10214  xrlttri3  10215  xrltne  10231  ngtmnft  10235  nmnfgt  10236  xrrebnd  10237  z2ge  10244  xltnegi  10253  xltadd1  10294  xsubge0  10299  xleaddadd  10305  ixxval  10314  elixx1  10315  elioo2  10339  iccid  10343  iccsupr  10384  repos  10388  fzval  10429  elfz1  10432  fzm1  10523  zsupcllemstep  10678  suprzubdc  10687  zsupssdc  10689  qdclt  10696  exbtwnzlemstep  10698  exbtwnzlemex  10700  qbtwnre  10707  qbtwnxr  10708  flval  10723  apbtwnz  10725  flaplt  10738  modqid2  10808  modqmuladdnn0  10825  exp3val  10998  expge0  11032  expge1  11033  nn0ltexp2  11168  facdiv  11197  facwordi  11199  hashinfom  11238  hashennn  11240  hashunlem  11265  zfz1iso  11314  wrdlen1  11363  fstwrdne0  11365  wrdl1exs1  11418  pfxsuffeqwrdeq  11491  pfxsuff1eqwrdeq  11492  ccats1pfxeq  11507  ccats1pfxeqrex  11508  pfxccatin12lem3  11525  ovshftex  11605  shftfibg  11606  shftfib  11609  shftfn  11610  2shfti  11617  sqrt0rlem  11790  resqrexlemex  11812  rsqrmo  11814  resqrtcl  11816  rersqrtthlem  11817  sqrtsq  11831  cau3lem  11902  caubnd2  11905  maxleim  11993  maxabslemval  11996  maxleast  12001  maxleb  12004  fimaxre2  12015  fiidxsupcl  12017  minmax  12019  xrmaxleim  12034  xrmaxiflemval  12040  xrmaxaddlem  12050  xrminmax  12055  xrbdtri  12066  climi  12077  climeu  12086  climmo  12088  2clim  12091  addcn2  12100  mulcn2  12102  reccn2ap  12103  cn1lem  12104  summodc  12174  zsumdc  12175  fsum3  12178  cvgratz  12323  ntrivcvgap0  12340  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  sinltxirr  12552  dvdsabsb  12601  0dvds  12602  alzdvds  12645  dvdsext  12646  fzo0dvdseq  12648  2tp1odd  12675  2teven  12678  divalglemnn  12709  divalglemeunn  12712  divalglemeuneg  12714  bitsinv1lem  12752  gcdval  12760  gcddvds  12764  bezoutlemstep  12798  bezoutlemmain  12799  bezoutlemex  12802  bezoutlemeu  12808  bezoutlemsup  12810  dfgcd3  12811  bezout  12812  dvdsgcd  12813  dfgcd2  12815  dvdssq  12832  uzwodc  12838  nnwofdc  12839  lcmval  12865  lcmcllem  12869  dvdslcm  12871  lcmledvds  12872  lcmgcdlem  12879  lcmdvds  12881  coprmgcdb  12890  coprmdvds2  12895  cncongr1  12905  cncongr2  12906  isprm  12911  dvdsnprmd  12927  dvdsprm  12940  exprmfct  12941  isprm6  12950  prmexpb  12954  prmfac1  12955  rpexp  12956  sqrt2irr  12965  nnmaxpwlemparts  12976  nnmaxpw  12977  sqpweven  12979  2sqpwodd  12980  sqne2sq  12981  nnoddn2prmb  13069  pceu  13102  pczpre  13104  pcdiv  13109  pcdvdsb  13127  difsqpwdvds  13145  pcmpt  13150  pcmptdvds  13152  oddprmdvds  13161  prmpwdvds  13162  infpnlem2  13167  ballotfilemfcc  13290  oddennn  13340  evenennn  13341  exmidunben  13374  nninfdclemcl  13396  nninfdclemp1  13398  nninfdc  13401  infpn2  13404  eqgen  14088  zndvds  15092  znleval  15096  psrbagmaxlem1  15178  psrass1filem  15186  psrmulvalfi  15197  comet  15742  metcnpi  15758  metcnpi2  15759  metcnpi3  15760  addcncntoplem  15804  cncfi  15821  elcncf1di  15822  mulcncflem  15850  dedekindeulemuub  15860  dedekindeulemloc  15862  dedekindeulemlu  15864  dedekindeulemeu  15865  dedekindeu  15866  suplociccreex  15867  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemloc  15871  dedekindicclemlu  15873  dedekindicclemeu  15874  dedekindicclemicc  15875  dedekindicc  15876  ivthinclemlopn  15879  ivthinclemlr  15880  ivthinclemuopn  15881  ivthinclemur  15882  ivthinclemloc  15884  ivthinc  15886  ivthreinc  15888  dich0  15895  ivthdich  15896  limcimo  15908  cnplimclemr  15912  limccnp2lem  15919  limccoap  15921  eldvap  15925  logltb  16121  zprmlogbaplem3  16234  zprmlogbap  16235  pellexlem3  16248  ppiublem1  16308  chtqub  16313  bpos1lem  16326  bposlem9  16336  lgsdir  16376  lgsne0  16379  gausslemma2dlem0i  16398  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  2lgslem2  16433  2lgs  16445  2sqlem6  16461  2sqlem8  16464  2sqlem10  16466  lfgredg2dom  16595  istrl  16848  clwwlkn0  16871  clwwlkext2edg  16885  clwwlknonccat  16896  clwwlknonex2  16902  iseupth  16910  konigsberg  16956  lealltlt2  16974  sbthom  17294  rirrdisj  17308  trilpo  17316  trirec0  17317  apdiff  17321  reap0  17332  cndcap  17333  nconstwlpolem  17339  neapmkv  17342  neap0mkv  17343  ltlenmkv  17344