Theorem breq2 4008

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

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

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 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-br 4005

This theorem is referenced by:  breq12  4009  breq2i  4012  breq2d  4016  nbrne1  4023  brralrspcev  4062  brimralrspcev  4063  pocl  4304  swopolem  4306  swopo  4307  sowlin  4321  sotricim  4324  sotritrieq  4326  seex  4336  frind  4353  wetriext  4577  vtoclr  4675  posng  4699  brcog  4795  brcogw  4797  opelcnvg  4808  dfdmf  4821  breldmg  4834  dfrnf  4869  dmcoss  4897  resieq  4918  dfres2  4960  elimag  4975  elrelimasn  4995  elimasn  4996  intirr  5016  poirr2  5022  poltletr  5030  dffun6f  5230  dffun4f  5233  fun11  5284  brprcneu  5509  fv3  5539  tz6.12c  5546  relelfvdm  5548  funbrfv  5555  fnbrfvb  5557  funfvdm2f  5582  fndmdif  5622  dff3im  5662  fmptco  5683  foeqcnvco  5791  isorel  5809  isocnv  5812  isotr  5817  isopolem  5823  isosolem  5825  f1oiso  5827  f1oiso2  5828  caovordig  6040  caovordg  6042  caovord  6046  caofrss  6107  caoftrn  6108  poxp  6233  tposoprab  6281  ertr  6550  ecopovsym  6631  ecopovtrn  6632  ecopovsymg  6634  ecopovtrng  6635  th3qlem2  6638  domeng  6752  eqeng  6766  snfig  6814  nneneq  6857  nnfi  6872  ssfilem  6875  domfiexmid  6878  dif1enen  6880  diffitest  6887  findcard  6888  findcard2  6889  findcard2s  6890  diffisn  6893  tridc  6899  fimax2gtrilemstep  6900  inffiexmid  6906  unsnfi  6918  fiintim  6928  fisseneq  6931  isbth  6966  supmoti  6992  eqsupti  6995  supubti  6998  suplubti  6999  suplub2ti  7000  supmaxti  7003  supsnti  7004  isotilem  7005  isoti  7006  supisolem  7007  supisoex  7008  cardcl  7180  isnumi  7181  cardval3ex  7184  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidapne  7259  nqtri3or  7395  ltsonq  7397  ltanqg  7399  ltmnqg  7400  ltexnqq  7407  nsmallnqq  7411  subhalfnqq  7413  ltbtwnnqq  7414  prarloclemarch2  7418  nqnq0pi  7437  prcdnql  7483  prcunqu  7484  prnminu  7488  genpcdl  7518  genprndl  7520  genprndu  7521  genpdisj  7522  nqprm  7541  nqprrnd  7542  nqprdisj  7543  nqprloc  7544  nqprlu  7546  nqprl  7550  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  1idpru  7590  ltnqpr  7592  ltnqpri  7593  prplnqu  7619  recexprlemelu  7622  recexprlemm  7623  recexprlemloc  7630  recexprlem1ssl  7632  recexprlemss1u  7635  cauappcvgprlemm  7644  cauappcvgprlemopu  7647  cauappcvgprlemupu  7648  cauappcvgprlemdisj  7650  cauappcvgprlemloc  7651  cauappcvgprlemladdfu  7653  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem2  7659  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopu  7670  caucvgprlemupu  7671  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprlem2  7679  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnbj  7692  caucvgprprlemmu  7694  caucvgprprlemexbt  7705  caucvgprprlemaddq  7707  caucvgprprlem1  7708  caucvgprprlem2  7709  suplocexprlemmu  7717  suplocexprlemru  7718  suplocexprlemdisj  7719  suplocexprlemloc  7720  suplocexprlemub  7722  suplocexpr  7724  lttrsr  7761  ltsosr  7763  ltasrg  7769  recexgt0sr  7772  mulgt0sr  7777  aptisr  7778  mulextsr1  7780  srpospr  7782  caucvgsrlemgt1  7794  caucvgsrlemoffres  7799  caucvgsr  7801  map2psrprg  7804  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  axprecex  7879  axpre-ltwlin  7882  axpre-lttrn  7883  axpre-apti  7884  axpre-ltadd  7885  axpre-mulgt0  7886  axpre-mulext  7887  axcaucvglemcau  7897  axcaucvglemres  7898  axcaucvg  7899  axpre-suploclemres  7900  axpre-suploc  7901  ltxrlt  8023  lttri3  8037  ltne  8042  eqle  8049  ltordlem  8439  reapti  8536  apreim  8560  squeeze0  8861  lbreu  8902  lble  8904  suprleubex  8911  sup3exmid  8914  nnge1  8942  nn2ge  8952  nn1gt1  8953  nnsub  8958  nominpos  9156  nn0ge0  9201  elnnnn0b  9220  nn0ge2m1nn  9236  zdclt  9330  suprzclex  9351  peano2uz2  9360  peano5uzti  9361  dfuzi  9363  uzind  9364  uzind3  9366  eluz1  9532  uzind4  9588  indstr  9593  supinfneg  9595  infsupneg  9596  infregelbex  9598  indstr2  9609  ublbneg  9613  elpq  9648  elpqb  9649  elrp  9655  mnfltxr  9786  nn0pnfge0  9791  xrltnsym  9793  xrlttr  9795  xrltso  9796  xrlttri3  9797  xrltne  9813  ngtmnft  9817  nmnfgt  9818  xrrebnd  9819  z2ge  9826  xltnegi  9835  xltadd1  9876  xsubge0  9881  xleaddadd  9887  ixxval  9896  elixx1  9897  elioo2  9921  iccid  9925  iccsupr  9966  repos  9970  fzval  10010  elfz1  10013  fzm1  10100  exbtwnzlemstep  10248  exbtwnzlemex  10250  qbtwnre  10257  qbtwnxr  10258  flval  10272  apbtwnz  10274  modqid2  10351  modqmuladdnn0  10368  exp3val  10522  expge0  10556  expge1  10557  nn0ltexp2  10689  facdiv  10718  facwordi  10720  hashinfom  10758  hashennn  10760  hashunlem  10784  zfz1iso  10821  ovshftex  10828  shftfibg  10829  shftfib  10832  shftfn  10833  2shfti  10840  sqrt0rlem  11012  resqrexlemex  11034  rsqrmo  11036  resqrtcl  11038  rersqrtthlem  11039  sqrtsq  11053  cau3lem  11123  caubnd2  11126  maxleim  11214  maxabslemval  11217  maxleast  11222  maxleb  11225  fimaxre2  11235  minmax  11238  xrmaxleim  11252  xrmaxiflemval  11258  xrmaxaddlem  11268  xrminmax  11273  xrbdtri  11284  climi  11295  climeu  11304  climmo  11306  2clim  11309  addcn2  11318  mulcn2  11320  reccn2ap  11321  cn1lem  11322  summodc  11391  zsumdc  11392  fsum3  11395  cvgratz  11540  ntrivcvgap0  11557  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  dvdsabsb  11817  0dvds  11818  alzdvds  11860  dvdsext  11861  fzo0dvdseq  11863  2tp1odd  11889  2teven  11892  divalglemnn  11923  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  suprzubdc  11953  zsupssdc  11955  gcdval  11960  gcddvds  11964  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlemex  12002  bezoutlemeu  12008  bezoutlemsup  12010  dfgcd3  12011  bezout  12012  dvdsgcd  12013  dfgcd2  12015  dvdssq  12032  uzwodc  12038  nnwofdc  12039  lcmval  12063  lcmcllem  12067  dvdslcm  12069  lcmledvds  12070  lcmgcdlem  12077  lcmdvds  12079  coprmgcdb  12088  coprmdvds2  12093  cncongr1  12103  cncongr2  12104  isprm  12109  dvdsnprmd  12125  dvdsprm  12137  exprmfct  12138  isprm6  12147  prmexpb  12151  prmfac1  12152  rpexp  12153  sqrt2irr  12162  oddpwdclemdc  12173  oddpwdc  12174  sqpweven  12175  2sqpwodd  12176  sqne2sq  12177  nnoddn2prmb  12262  pceu  12295  pczpre  12297  pcdiv  12302  pcdvdsb  12319  difsqpwdvds  12337  pcmpt  12341  pcmptdvds  12343  oddprmdvds  12352  prmpwdvds  12353  infpnlem2  12358  oddennn  12393  evenennn  12394  exmidunben  12427  nninfdclemcl  12449  nninfdclemp1  12451  nninfdc  12454  infpn2  12457  eqgen  13086  comet  14002  metcnpi  14018  metcnpi2  14019  metcnpi3  14020  addcncntoplem  14054  cncfi  14068  elcncf1di  14069  mulcncflem  14093  dedekindeulemuub  14098  dedekindeulemloc  14100  dedekindeulemlu  14102  dedekindeulemeu  14103  dedekindeu  14104  suplociccreex  14105  suplociccex  14106  dedekindicclemuub  14107  dedekindicclemloc  14109  dedekindicclemlu  14111  dedekindicclemeu  14112  dedekindicclemicc  14113  dedekindicc  14114  ivthinclemlopn  14117  ivthinclemlr  14118  ivthinclemuopn  14119  ivthinclemur  14120  ivthinclemloc  14122  ivthinc  14124  limcimo  14137  cnplimclemr  14141  limccnp2lem  14148  limccoap  14150  eldvap  14154  logltb  14298  lgsdir  14439  lgsne0  14442  2sqlem6  14470  2sqlem8  14473  2sqlem10  14475  sbthom  14777  trilpo  14794  trirec0  14795  apdiff  14799  reap0  14809  nconstwlpolem  14815  neapmkv  14818  neap0mkv  14819  ltlenmkv  14820