Theorem breq2 4005

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

Assertion

Ref	Expression
breq2	⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Proof of Theorem breq2

Step	Hyp	Ref	Expression
1		opeq2 3778	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2246	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 4002	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 4002	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353   ∈ wcel 2148  ⟨cop 3595   class class class wbr 4001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002

This theorem is referenced by:  breq12  4006  breq2i  4009  breq2d  4013  nbrne1  4020  brralrspcev  4059  brimralrspcev  4060  pocl  4301  swopolem  4303  swopo  4304  sowlin  4318  sotricim  4321  sotritrieq  4323  seex  4333  frind  4350  wetriext  4574  vtoclr  4672  posng  4696  brcog  4791  brcogw  4793  opelcnvg  4804  dfdmf  4817  breldmg  4830  dfrnf  4865  dmcoss  4893  resieq  4914  dfres2  4956  elimag  4971  elrelimasn  4991  elimasn  4992  intirr  5012  poirr2  5018  poltletr  5026  dffun6f  5226  dffun4f  5229  fun11  5280  brprcneu  5505  fv3  5535  tz6.12c  5542  relelfvdm  5544  funbrfv  5551  fnbrfvb  5553  funfvdm2f  5578  fndmdif  5618  dff3im  5658  fmptco  5679  foeqcnvco  5786  isorel  5804  isocnv  5807  isotr  5812  isopolem  5818  isosolem  5820  f1oiso  5822  f1oiso2  5823  caovordig  6035  caovordg  6037  caovord  6041  caofrss  6102  caoftrn  6103  poxp  6228  tposoprab  6276  ertr  6545  ecopovsym  6626  ecopovtrn  6627  ecopovsymg  6629  ecopovtrng  6630  th3qlem2  6633  domeng  6747  eqeng  6761  snfig  6809  nneneq  6852  nnfi  6867  ssfilem  6870  domfiexmid  6873  dif1enen  6875  diffitest  6882  findcard  6883  findcard2  6884  findcard2s  6885  diffisn  6888  tridc  6894  fimax2gtrilemstep  6895  inffiexmid  6901  unsnfi  6913  fiintim  6923  fisseneq  6926  isbth  6961  supmoti  6987  eqsupti  6990  supubti  6993  suplubti  6994  suplub2ti  6995  supmaxti  6998  supsnti  6999  isotilem  7000  isoti  7001  supisolem  7002  supisoex  7003  cardcl  7175  isnumi  7176  cardval3ex  7179  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidapne  7254  nqtri3or  7390  ltsonq  7392  ltanqg  7394  ltmnqg  7395  ltexnqq  7402  nsmallnqq  7406  subhalfnqq  7408  ltbtwnnqq  7409  prarloclemarch2  7413  nqnq0pi  7432  prcdnql  7478  prcunqu  7479  prnminu  7483  genpcdl  7513  genprndl  7515  genprndu  7516  genpdisj  7517  nqprm  7536  nqprrnd  7537  nqprdisj  7538  nqprloc  7539  nqprlu  7541  nqprl  7545  addnqprlemru  7552  addnqprlemfl  7553  addnqprlemfu  7554  mulnqprlemru  7568  mulnqprlemfl  7569  mulnqprlemfu  7570  1idpru  7585  ltnqpr  7587  ltnqpri  7588  prplnqu  7614  recexprlemelu  7617  recexprlemm  7618  recexprlemloc  7625  recexprlem1ssl  7627  recexprlemss1u  7630  cauappcvgprlemm  7639  cauappcvgprlemopu  7642  cauappcvgprlemupu  7643  cauappcvgprlemdisj  7645  cauappcvgprlemloc  7646  cauappcvgprlemladdfu  7648  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem2  7654  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemopu  7665  caucvgprlemupu  7666  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  caucvgprlem2  7674  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnbj  7687  caucvgprprlemmu  7689  caucvgprprlemexbt  7700  caucvgprprlemaddq  7702  caucvgprprlem1  7703  caucvgprprlem2  7704  suplocexprlemmu  7712  suplocexprlemru  7713  suplocexprlemdisj  7714  suplocexprlemloc  7715  suplocexprlemub  7717  suplocexpr  7719  lttrsr  7756  ltsosr  7758  ltasrg  7764  recexgt0sr  7767  mulgt0sr  7772  aptisr  7773  mulextsr1  7775  srpospr  7777  caucvgsrlemgt1  7789  caucvgsrlemoffres  7794  caucvgsr  7796  map2psrprg  7799  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  axprecex  7874  axpre-ltwlin  7877  axpre-lttrn  7878  axpre-apti  7879  axpre-ltadd  7880  axpre-mulgt0  7881  axpre-mulext  7882  axcaucvglemcau  7892  axcaucvglemres  7893  axcaucvg  7894  axpre-suploclemres  7895  axpre-suploc  7896  ltxrlt  8017  lttri3  8031  ltne  8036  eqle  8043  ltordlem  8433  reapti  8530  apreim  8554  squeeze0  8855  lbreu  8896  lble  8898  suprleubex  8905  sup3exmid  8908  nnge1  8936  nn2ge  8946  nn1gt1  8947  nnsub  8952  nominpos  9150  nn0ge0  9195  elnnnn0b  9214  nn0ge2m1nn  9230  zdclt  9324  suprzclex  9345  peano2uz2  9354  peano5uzti  9355  dfuzi  9357  uzind  9358  uzind3  9360  eluz1  9526  uzind4  9582  indstr  9587  supinfneg  9589  infsupneg  9590  infregelbex  9592  indstr2  9603  ublbneg  9607  elpq  9642  elpqb  9643  elrp  9649  mnfltxr  9780  nn0pnfge0  9785  xrltnsym  9787  xrlttr  9789  xrltso  9790  xrlttri3  9791  xrltne  9807  ngtmnft  9811  nmnfgt  9812  xrrebnd  9813  z2ge  9820  xltnegi  9829  xltadd1  9870  xsubge0  9875  xleaddadd  9881  ixxval  9890  elixx1  9891  elioo2  9915  iccid  9919  iccsupr  9960  repos  9964  fzval  10004  elfz1  10007  fzm1  10093  exbtwnzlemstep  10241  exbtwnzlemex  10243  qbtwnre  10250  qbtwnxr  10251  flval  10265  apbtwnz  10267  modqid2  10344  modqmuladdnn0  10361  exp3val  10515  expge0  10549  expge1  10550  nn0ltexp2  10681  facdiv  10709  facwordi  10711  hashinfom  10749  hashennn  10751  hashunlem  10775  zfz1iso  10812  ovshftex  10819  shftfibg  10820  shftfib  10823  shftfn  10824  2shfti  10831  sqrt0rlem  11003  resqrexlemex  11025  rsqrmo  11027  resqrtcl  11029  rersqrtthlem  11030  sqrtsq  11044  cau3lem  11114  caubnd2  11117  maxleim  11205  maxabslemval  11208  maxleast  11213  maxleb  11216  fimaxre2  11226  minmax  11229  xrmaxleim  11243  xrmaxiflemval  11249  xrmaxaddlem  11259  xrminmax  11264  xrbdtri  11275  climi  11286  climeu  11295  climmo  11297  2clim  11300  addcn2  11309  mulcn2  11311  reccn2ap  11312  cn1lem  11313  summodc  11382  zsumdc  11383  fsum3  11386  cvgratz  11531  ntrivcvgap0  11548  prodmodc  11577  zproddc  11578  fprodseq  11582  fprodntrivap  11583  dvdsabsb  11808  0dvds  11809  alzdvds  11850  dvdsext  11851  fzo0dvdseq  11853  2tp1odd  11879  2teven  11882  divalglemnn  11913  divalglemeunn  11916  divalglemeuneg  11918  zsupcllemstep  11936  suprzubdc  11943  zsupssdc  11945  gcdval  11950  gcddvds  11954  bezoutlemstep  11988  bezoutlemmain  11989  bezoutlemex  11992  bezoutlemeu  11998  bezoutlemsup  12000  dfgcd3  12001  bezout  12002  dvdsgcd  12003  dfgcd2  12005  dvdssq  12022  uzwodc  12028  nnwofdc  12029  lcmval  12053  lcmcllem  12057  dvdslcm  12059  lcmledvds  12060  lcmgcdlem  12067  lcmdvds  12069  coprmgcdb  12078  coprmdvds2  12083  cncongr1  12093  cncongr2  12094  isprm  12099  dvdsnprmd  12115  dvdsprm  12127  exprmfct  12128  isprm6  12137  prmexpb  12141  prmfac1  12142  rpexp  12143  sqrt2irr  12152  oddpwdclemdc  12163  oddpwdc  12164  sqpweven  12165  2sqpwodd  12166  sqne2sq  12167  nnoddn2prmb  12252  pceu  12285  pczpre  12287  pcdiv  12292  pcdvdsb  12309  difsqpwdvds  12327  pcmpt  12331  pcmptdvds  12333  oddprmdvds  12342  prmpwdvds  12343  infpnlem2  12348  oddennn  12383  evenennn  12384  exmidunben  12417  nninfdclemcl  12439  nninfdclemp1  12441  nninfdc  12444  infpn2  12447  comet  13781  metcnpi  13797  metcnpi2  13798  metcnpi3  13799  addcncntoplem  13833  cncfi  13847  elcncf1di  13848  mulcncflem  13872  dedekindeulemuub  13877  dedekindeulemloc  13879  dedekindeulemlu  13881  dedekindeulemeu  13882  dedekindeu  13883  suplociccreex  13884  suplociccex  13885  dedekindicclemuub  13886  dedekindicclemloc  13888  dedekindicclemlu  13890  dedekindicclemeu  13891  dedekindicclemicc  13892  dedekindicc  13893  ivthinclemlopn  13896  ivthinclemlr  13897  ivthinclemuopn  13898  ivthinclemur  13899  ivthinclemloc  13901  ivthinc  13903  limcimo  13916  cnplimclemr  13920  limccnp2lem  13927  limccoap  13929  eldvap  13933  logltb  14077  lgsdir  14218  lgsne0  14221  2sqlem6  14238  2sqlem8  14241  2sqlem10  14243  sbthom  14545  trilpo  14562  trirec0  14563  apdiff  14567  reap0  14577  nconstwlpolem  14583  neapmkv  14586  neap0mkv  14587  ltlenmkv  14588