Theorem breq2 4092

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 3863	. . 3 ⊢ (𝐴 = 𝐵 → ⟨𝐶, 𝐴⟩ = ⟨𝐶, 𝐵⟩)
2	1	eleq1d 2300	. 2 ⊢ (𝐴 = 𝐵 → (⟨𝐶, 𝐴⟩ ∈ 𝑅 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅))
3		df-br 4089	. 2 ⊢ (𝐶𝑅𝐴 ↔ ⟨𝐶, 𝐴⟩ ∈ 𝑅)
4		df-br 4089	. 2 ⊢ (𝐶𝑅𝐵 ↔ ⟨𝐶, 𝐵⟩ ∈ 𝑅)
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐶𝑅𝐴 ↔ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ∈ wcel 2202  ⟨cop 3672   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  breq12  4093  breq2i  4096  breq2d  4100  nbrne1  4107  brralrspcev  4147  brimralrspcev  4148  pocl  4400  swopolem  4402  swopo  4403  sowlin  4417  sotricim  4420  sotritrieq  4422  seex  4432  frind  4449  wetriext  4675  vtoclr  4774  posng  4798  brcog  4897  brcogw  4899  opelcnvg  4910  dfdmf  4924  breldmg  4937  dfrnf  4973  dmcoss  5002  resieq  5023  dfres2  5065  elimag  5080  elrelimasn  5102  elimasn  5103  intirr  5123  poirr2  5129  poltletr  5137  dffun6f  5339  dffun4f  5342  fun11  5397  brprcneu  5632  fv3  5662  tz6.12c  5669  relelfvdm  5671  fvmbr  5674  funbrfv  5682  fnbrfvb  5684  funfvdm2f  5711  fndmdif  5752  dff3im  5792  fmptco  5813  foeqcnvco  5930  isorel  5948  isocnv  5951  isotr  5956  isopolem  5962  isosolem  5964  f1oiso  5966  f1oiso2  5967  caovordig  6187  caovordg  6189  caovord  6193  caofrss  6266  caoftrn  6267  poxp  6396  tposoprab  6445  ertr  6716  ecopovsym  6799  ecopovtrn  6800  ecopovsymg  6802  ecopovtrng  6803  th3qlem2  6806  domeng  6922  eqeng  6938  snfig  6988  nneneq  7042  nnfi  7058  ssfilem  7061  ssfilemd  7063  domfiexmid  7066  dif1enen  7068  diffitest  7075  findcard  7076  findcard2  7077  findcard2s  7078  diffisn  7081  tridc  7088  fimax2gtrilemstep  7089  inffiexmid  7097  unsnfi  7110  fiintim  7122  fisseneq  7126  isbth  7165  supmoti  7191  eqsupti  7194  supubti  7197  suplubti  7198  suplub2ti  7199  supmaxti  7202  supsnti  7203  isotilem  7204  isoti  7205  supisolem  7206  supisoex  7207  cardcl  7384  isnumi  7385  cardval3ex  7388  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidapne  7478  nqtri3or  7615  ltsonq  7617  ltanqg  7619  ltmnqg  7620  ltexnqq  7627  nsmallnqq  7631  subhalfnqq  7633  ltbtwnnqq  7634  prarloclemarch2  7638  nqnq0pi  7657  prcdnql  7703  prcunqu  7704  prnminu  7708  genpcdl  7738  genprndl  7740  genprndu  7741  genpdisj  7742  nqprm  7761  nqprrnd  7762  nqprdisj  7763  nqprloc  7764  nqprlu  7766  nqprl  7770  addnqprlemru  7777  addnqprlemfl  7778  addnqprlemfu  7779  mulnqprlemru  7793  mulnqprlemfl  7794  mulnqprlemfu  7795  1idpru  7810  ltnqpr  7812  ltnqpri  7813  prplnqu  7839  recexprlemelu  7842  recexprlemm  7843  recexprlemloc  7850  recexprlem1ssl  7852  recexprlemss1u  7855  cauappcvgprlemm  7864  cauappcvgprlemopu  7867  cauappcvgprlemupu  7868  cauappcvgprlemdisj  7870  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  cauappcvgprlem2  7879  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopu  7890  caucvgprlemupu  7891  caucvgprlemdisj  7893  caucvgprlemloc  7894  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem2  7899  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnbj  7912  caucvgprprlemmu  7914  caucvgprprlemexbt  7925  caucvgprprlemaddq  7927  caucvgprprlem1  7928  caucvgprprlem2  7929  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexpr  7944  lttrsr  7981  ltsosr  7983  ltasrg  7989  recexgt0sr  7992  mulgt0sr  7997  aptisr  7998  mulextsr1  8000  srpospr  8002  caucvgsrlemgt1  8014  caucvgsrlemoffres  8019  caucvgsr  8021  map2psrprg  8024  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  axprecex  8099  axpre-ltwlin  8102  axpre-lttrn  8103  axpre-apti  8104  axpre-ltadd  8105  axpre-mulgt0  8106  axpre-mulext  8107  axcaucvglemcau  8117  axcaucvglemres  8118  axcaucvg  8119  axpre-suploclemres  8120  axpre-suploc  8121  ltxrlt  8244  lttri3  8258  ltne  8263  eqle  8270  ltordlem  8661  reapti  8758  apreim  8782  squeeze0  9083  lbreu  9124  lble  9126  suprleubex  9133  sup3exmid  9136  nnge1  9165  nn2ge  9175  nn1gt1  9176  nnsub  9181  nominpos  9381  nn0ge0  9426  elnnnn0b  9445  nn0ge2m1nn  9461  zdclt  9556  suprzclex  9577  peano2uz2  9586  peano5uzti  9587  dfuzi  9589  uzind  9590  uzind3  9592  eluz1  9758  uzind4  9821  indstr  9826  supinfneg  9828  infsupneg  9829  infregelbex  9831  indstr2  9842  ublbneg  9846  irrmulap  9881  elpq  9882  elpqb  9883  elrp  9889  mnfltxr  10020  nn0pnfge0  10025  xrltnsym  10027  xrlttr  10029  xrltso  10030  xrlttri3  10031  xrltne  10047  ngtmnft  10051  nmnfgt  10052  xrrebnd  10053  z2ge  10060  xltnegi  10069  xltadd1  10110  xsubge0  10115  xleaddadd  10121  ixxval  10130  elixx1  10131  elioo2  10155  iccid  10159  iccsupr  10200  repos  10204  fzval  10244  elfz1  10247  fzm1  10334  zsupcllemstep  10488  suprzubdc  10495  zsupssdc  10497  qdclt  10504  exbtwnzlemstep  10506  exbtwnzlemex  10508  qbtwnre  10515  qbtwnxr  10516  flval  10531  apbtwnz  10533  modqid2  10612  modqmuladdnn0  10629  exp3val  10802  expge0  10836  expge1  10837  nn0ltexp2  10970  facdiv  10999  facwordi  11001  hashinfom  11039  hashennn  11041  hashunlem  11066  zfz1iso  11104  wrdlen1  11150  fstwrdne0  11152  wrdl1exs1  11205  pfxsuffeqwrdeq  11278  pfxsuff1eqwrdeq  11279  ccats1pfxeq  11294  ccats1pfxeqrex  11295  pfxccatin12lem3  11312  ovshftex  11379  shftfibg  11380  shftfib  11383  shftfn  11384  2shfti  11391  sqrt0rlem  11563  resqrexlemex  11585  rsqrmo  11587  resqrtcl  11589  rersqrtthlem  11590  sqrtsq  11604  cau3lem  11674  caubnd2  11677  maxleim  11765  maxabslemval  11768  maxleast  11773  maxleb  11776  fimaxre2  11787  minmax  11790  xrmaxleim  11804  xrmaxiflemval  11810  xrmaxaddlem  11820  xrminmax  11825  xrbdtri  11836  climi  11847  climeu  11856  climmo  11858  2clim  11861  addcn2  11870  mulcn2  11872  reccn2ap  11873  cn1lem  11874  summodc  11943  zsumdc  11944  fsum3  11947  cvgratz  12092  ntrivcvgap0  12109  prodmodc  12138  zproddc  12139  fprodseq  12143  fprodntrivap  12144  sinltxirr  12321  dvdsabsb  12370  0dvds  12371  alzdvds  12414  dvdsext  12415  fzo0dvdseq  12417  2tp1odd  12444  2teven  12447  divalglemnn  12478  divalglemeunn  12481  divalglemeuneg  12483  bitsinv1lem  12521  gcdval  12529  gcddvds  12533  bezoutlemstep  12567  bezoutlemmain  12568  bezoutlemex  12571  bezoutlemeu  12577  bezoutlemsup  12579  dfgcd3  12580  bezout  12581  dvdsgcd  12582  dfgcd2  12584  dvdssq  12601  uzwodc  12607  nnwofdc  12608  lcmval  12634  lcmcllem  12638  dvdslcm  12640  lcmledvds  12641  lcmgcdlem  12648  lcmdvds  12650  coprmgcdb  12659  coprmdvds2  12664  cncongr1  12674  cncongr2  12675  isprm  12680  dvdsnprmd  12696  dvdsprm  12708  exprmfct  12709  isprm6  12718  prmexpb  12722  prmfac1  12723  rpexp  12724  sqrt2irr  12733  oddpwdclemdc  12744  oddpwdc  12745  sqpweven  12746  2sqpwodd  12747  sqne2sq  12748  nnoddn2prmb  12834  pceu  12867  pczpre  12869  pcdiv  12874  pcdvdsb  12892  difsqpwdvds  12910  pcmpt  12915  pcmptdvds  12917  oddprmdvds  12926  prmpwdvds  12927  infpnlem2  12932  oddennn  13012  evenennn  13013  exmidunben  13046  nninfdclemcl  13068  nninfdclemp1  13070  nninfdc  13073  infpn2  13076  eqgen  13813  zndvds  14662  znleval  14666  comet  15222  metcnpi  15238  metcnpi2  15239  metcnpi3  15240  addcncntoplem  15284  cncfi  15301  elcncf1di  15302  mulcncflem  15330  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeulemeu  15345  dedekindeu  15346  suplociccreex  15347  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemeu  15354  dedekindicclemicc  15355  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemlr  15360  ivthinclemuopn  15361  ivthinclemur  15362  ivthinclemloc  15364  ivthinc  15366  ivthreinc  15368  dich0  15375  ivthdich  15376  limcimo  15388  cnplimclemr  15392  limccnp2lem  15399  limccoap  15401  eldvap  15405  logltb  15597  lgsdir  15763  lgsne0  15766  gausslemma2dlem0i  15785  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  2lgslem2  15820  2lgs  15832  2sqlem6  15848  2sqlem8  15851  2sqlem10  15853  lfgredg2dom  15982  istrl  16235  clwwlkn0  16258  clwwlkext2edg  16272  clwwlknonccat  16283  clwwlknonex2  16289  iseupth  16297  sbthom  16630  trilpo  16647  trirec0  16648  apdiff  16652  reap0  16662  cndcap  16663  nconstwlpolem  16669  neapmkv  16672  neap0mkv  16673  ltlenmkv  16674