Theorem breq2 4063

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2178  ⟨cop 3646   class class class wbr 4059

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-br 4060

This theorem is referenced by:  breq12  4064  breq2i  4067  breq2d  4071  nbrne1  4078  brralrspcev  4118  brimralrspcev  4119  pocl  4368  swopolem  4370  swopo  4371  sowlin  4385  sotricim  4388  sotritrieq  4390  seex  4400  frind  4417  wetriext  4643  vtoclr  4741  posng  4765  brcog  4863  brcogw  4865  opelcnvg  4876  dfdmf  4890  breldmg  4903  dfrnf  4938  dmcoss  4967  resieq  4988  dfres2  5030  elimag  5045  elrelimasn  5067  elimasn  5068  intirr  5088  poirr2  5094  poltletr  5102  dffun6f  5303  dffun4f  5306  fun11  5360  brprcneu  5592  fv3  5622  tz6.12c  5629  relelfvdm  5631  funbrfv  5640  fnbrfvb  5642  funfvdm2f  5667  fndmdif  5708  dff3im  5748  fmptco  5769  foeqcnvco  5882  isorel  5900  isocnv  5903  isotr  5908  isopolem  5914  isosolem  5916  f1oiso  5918  f1oiso2  5919  caovordig  6135  caovordg  6137  caovord  6141  caofrss  6213  caoftrn  6214  poxp  6341  tposoprab  6389  ertr  6658  ecopovsym  6741  ecopovtrn  6742  ecopovsymg  6744  ecopovtrng  6745  th3qlem2  6748  domeng  6864  eqeng  6880  snfig  6930  nneneq  6979  nnfi  6995  ssfilem  6998  domfiexmid  7001  dif1enen  7003  diffitest  7010  findcard  7011  findcard2  7012  findcard2s  7013  diffisn  7016  tridc  7022  fimax2gtrilemstep  7023  inffiexmid  7029  unsnfi  7042  fiintim  7054  fisseneq  7057  isbth  7095  supmoti  7121  eqsupti  7124  supubti  7127  suplubti  7128  suplub2ti  7129  supmaxti  7132  supsnti  7133  isotilem  7134  isoti  7135  supisolem  7136  supisoex  7137  cardcl  7314  isnumi  7315  cardval3ex  7318  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidapne  7407  nqtri3or  7544  ltsonq  7546  ltanqg  7548  ltmnqg  7549  ltexnqq  7556  nsmallnqq  7560  subhalfnqq  7562  ltbtwnnqq  7563  prarloclemarch2  7567  nqnq0pi  7586  prcdnql  7632  prcunqu  7633  prnminu  7637  genpcdl  7667  genprndl  7669  genprndu  7670  genpdisj  7671  nqprm  7690  nqprrnd  7691  nqprdisj  7692  nqprloc  7693  nqprlu  7695  nqprl  7699  addnqprlemru  7706  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemru  7722  mulnqprlemfl  7723  mulnqprlemfu  7724  1idpru  7739  ltnqpr  7741  ltnqpri  7742  prplnqu  7768  recexprlemelu  7771  recexprlemm  7772  recexprlemloc  7779  recexprlem1ssl  7781  recexprlemss1u  7784  cauappcvgprlemm  7793  cauappcvgprlemopu  7796  cauappcvgprlemupu  7797  cauappcvgprlemdisj  7799  cauappcvgprlemloc  7800  cauappcvgprlemladdfu  7802  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  cauappcvgprlem2  7808  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemopu  7819  caucvgprlemupu  7820  caucvgprlemdisj  7822  caucvgprlemloc  7823  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem2  7828  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnbj  7841  caucvgprprlemmu  7843  caucvgprprlemexbt  7854  caucvgprprlemaddq  7856  caucvgprprlem1  7857  caucvgprprlem2  7858  suplocexprlemmu  7866  suplocexprlemru  7867  suplocexprlemdisj  7868  suplocexprlemloc  7869  suplocexprlemub  7871  suplocexpr  7873  lttrsr  7910  ltsosr  7912  ltasrg  7918  recexgt0sr  7921  mulgt0sr  7926  aptisr  7927  mulextsr1  7929  srpospr  7931  caucvgsrlemgt1  7943  caucvgsrlemoffres  7948  caucvgsr  7950  map2psrprg  7953  suplocsrlemb  7954  suplocsrlempr  7955  suplocsrlem  7956  axprecex  8028  axpre-ltwlin  8031  axpre-lttrn  8032  axpre-apti  8033  axpre-ltadd  8034  axpre-mulgt0  8035  axpre-mulext  8036  axcaucvglemcau  8046  axcaucvglemres  8047  axcaucvg  8048  axpre-suploclemres  8049  axpre-suploc  8050  ltxrlt  8173  lttri3  8187  ltne  8192  eqle  8199  ltordlem  8590  reapti  8687  apreim  8711  squeeze0  9012  lbreu  9053  lble  9055  suprleubex  9062  sup3exmid  9065  nnge1  9094  nn2ge  9104  nn1gt1  9105  nnsub  9110  nominpos  9310  nn0ge0  9355  elnnnn0b  9374  nn0ge2m1nn  9390  zdclt  9485  suprzclex  9506  peano2uz2  9515  peano5uzti  9516  dfuzi  9518  uzind  9519  uzind3  9521  eluz1  9687  uzind4  9744  indstr  9749  supinfneg  9751  infsupneg  9752  infregelbex  9754  indstr2  9765  ublbneg  9769  irrmulap  9804  elpq  9805  elpqb  9806  elrp  9812  mnfltxr  9943  nn0pnfge0  9948  xrltnsym  9950  xrlttr  9952  xrltso  9953  xrlttri3  9954  xrltne  9970  ngtmnft  9974  nmnfgt  9975  xrrebnd  9976  z2ge  9983  xltnegi  9992  xltadd1  10033  xsubge0  10038  xleaddadd  10044  ixxval  10053  elixx1  10054  elioo2  10078  iccid  10082  iccsupr  10123  repos  10127  fzval  10167  elfz1  10170  fzm1  10257  zsupcllemstep  10409  suprzubdc  10416  zsupssdc  10418  qdclt  10425  exbtwnzlemstep  10427  exbtwnzlemex  10429  qbtwnre  10436  qbtwnxr  10437  flval  10452  apbtwnz  10454  modqid2  10533  modqmuladdnn0  10550  exp3val  10723  expge0  10757  expge1  10758  nn0ltexp2  10891  facdiv  10920  facwordi  10922  hashinfom  10960  hashennn  10962  hashunlem  10986  zfz1iso  11023  wrdlen1  11068  fstwrdne0  11070  wrdl1exs1  11121  pfxsuffeqwrdeq  11189  pfxsuff1eqwrdeq  11190  ccats1pfxeq  11205  ccats1pfxeqrex  11206  pfxccatin12lem3  11223  ovshftex  11245  shftfibg  11246  shftfib  11249  shftfn  11250  2shfti  11257  sqrt0rlem  11429  resqrexlemex  11451  rsqrmo  11453  resqrtcl  11455  rersqrtthlem  11456  sqrtsq  11470  cau3lem  11540  caubnd2  11543  maxleim  11631  maxabslemval  11634  maxleast  11639  maxleb  11642  fimaxre2  11653  minmax  11656  xrmaxleim  11670  xrmaxiflemval  11676  xrmaxaddlem  11686  xrminmax  11691  xrbdtri  11702  climi  11713  climeu  11722  climmo  11724  2clim  11727  addcn2  11736  mulcn2  11738  reccn2ap  11739  cn1lem  11740  summodc  11809  zsumdc  11810  fsum3  11813  cvgratz  11958  ntrivcvgap0  11975  prodmodc  12004  zproddc  12005  fprodseq  12009  fprodntrivap  12010  sinltxirr  12187  dvdsabsb  12236  0dvds  12237  alzdvds  12280  dvdsext  12281  fzo0dvdseq  12283  2tp1odd  12310  2teven  12313  divalglemnn  12344  divalglemeunn  12347  divalglemeuneg  12349  bitsinv1lem  12387  gcdval  12395  gcddvds  12399  bezoutlemstep  12433  bezoutlemmain  12434  bezoutlemex  12437  bezoutlemeu  12443  bezoutlemsup  12445  dfgcd3  12446  bezout  12447  dvdsgcd  12448  dfgcd2  12450  dvdssq  12467  uzwodc  12473  nnwofdc  12474  lcmval  12500  lcmcllem  12504  dvdslcm  12506  lcmledvds  12507  lcmgcdlem  12514  lcmdvds  12516  coprmgcdb  12525  coprmdvds2  12530  cncongr1  12540  cncongr2  12541  isprm  12546  dvdsnprmd  12562  dvdsprm  12574  exprmfct  12575  isprm6  12584  prmexpb  12588  prmfac1  12589  rpexp  12590  sqrt2irr  12599  oddpwdclemdc  12610  oddpwdc  12611  sqpweven  12612  2sqpwodd  12613  sqne2sq  12614  nnoddn2prmb  12700  pceu  12733  pczpre  12735  pcdiv  12740  pcdvdsb  12758  difsqpwdvds  12776  pcmpt  12781  pcmptdvds  12783  oddprmdvds  12792  prmpwdvds  12793  infpnlem2  12798  oddennn  12878  evenennn  12879  exmidunben  12912  nninfdclemcl  12934  nninfdclemp1  12936  nninfdc  12939  infpn2  12942  eqgen  13678  zndvds  14526  znleval  14530  comet  15086  metcnpi  15102  metcnpi2  15103  metcnpi3  15104  addcncntoplem  15148  cncfi  15165  elcncf1di  15166  mulcncflem  15194  dedekindeulemuub  15204  dedekindeulemloc  15206  dedekindeulemlu  15208  dedekindeulemeu  15209  dedekindeu  15210  suplociccreex  15211  suplociccex  15212  dedekindicclemuub  15213  dedekindicclemloc  15215  dedekindicclemlu  15217  dedekindicclemeu  15218  dedekindicclemicc  15219  dedekindicc  15220  ivthinclemlopn  15223  ivthinclemlr  15224  ivthinclemuopn  15225  ivthinclemur  15226  ivthinclemloc  15228  ivthinc  15230  ivthreinc  15232  dich0  15239  ivthdich  15240  limcimo  15252  cnplimclemr  15256  limccnp2lem  15263  limccoap  15265  eldvap  15269  logltb  15461  lgsdir  15627  lgsne0  15630  gausslemma2dlem0i  15649  lgsquadlem1  15669  lgsquadlem2  15670  lgsquadlem3  15671  2lgslem2  15684  2lgs  15696  2sqlem6  15712  2sqlem8  15715  2sqlem10  15717  lfgredg2dom  15838  sbthom  16167  trilpo  16184  trirec0  16185  apdiff  16189  reap0  16199  cndcap  16200  nconstwlpolem  16206  neapmkv  16209  neap0mkv  16210  ltlenmkv  16211