Theorem breq2 3789

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284   ∈ wcel 1433  ⟨cop 3401   class class class wbr 3785

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-br 3786

This theorem is referenced by:  breq12  3790  breq2i  3793  breq2d  3797  nbrne1  3802  pocl  4058  swopolem  4060  swopo  4061  sowlin  4075  sotricim  4078  sotritrieq  4080  seex  4090  frind  4107  wetriext  4319  vtoclr  4406  posng  4430  brcog  4520  brcogw  4522  opelcnvg  4533  dfdmf  4546  breldmg  4559  dfrnf  4593  dmcoss  4619  resieq  4640  dfres2  4678  elimag  4692  elreimasng  4711  elimasn  4712  intirr  4731  poirr2  4737  poltletr  4745  dffun6f  4935  dffun4f  4938  fun11  4986  brprcneu  5191  fv3  5218  tz6.12c  5224  relelfvdm  5226  funbrfv  5233  fnbrfvb  5235  funfvdm2f  5259  fndmdif  5293  dff3im  5333  fmptco  5351  foeqcnvco  5450  isorel  5468  isocnv  5471  isotr  5476  isopolem  5481  isosolem  5483  f1oiso  5485  f1oiso2  5486  caovordig  5686  caovordg  5688  caovord  5692  caofrss  5755  caoftrn  5756  poxp  5873  tposoprab  5918  ertr  6144  ecopovsym  6225  ecopovtrn  6226  ecopovsymg  6228  ecopovtrng  6229  th3qlem2  6232  domeng  6256  eqeng  6269  snfig  6314  nneneq  6343  nnfi  6357  ssfilem  6360  domfiexmid  6363  diffitest  6371  findcard  6372  findcard2  6373  findcard2s  6374  diffisn  6377  unsnfi  6384  supmoti  6406  eqsupti  6409  supubti  6412  suplubti  6413  suplub2ti  6414  supmaxti  6417  supsnti  6418  isotilem  6419  isoti  6420  supisolem  6421  supisoex  6422  cardcl  6450  isnumi  6451  cardval3ex  6454  nqtri3or  6586  ltsonq  6588  ltanqg  6590  ltmnqg  6591  ltexnqq  6598  nsmallnqq  6602  subhalfnqq  6604  ltbtwnnqq  6605  prarloclemarch2  6609  nqnq0pi  6628  prcdnql  6674  prcunqu  6675  prnminu  6679  genpcdl  6709  genprndl  6711  genprndu  6712  genpdisj  6713  nqprm  6732  nqprrnd  6733  nqprdisj  6734  nqprloc  6735  nqprlu  6737  nqprl  6741  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  1idpru  6781  ltnqpr  6783  ltnqpri  6784  prplnqu  6810  recexprlemelu  6813  recexprlemm  6814  recexprlemloc  6821  recexprlem1ssl  6823  recexprlemss1u  6826  cauappcvgprlemm  6835  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem2  6850  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprlem2  6870  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnbj  6883  caucvgprprlemmu  6885  caucvgprprlemexbt  6896  caucvgprprlemaddq  6898  caucvgprprlem1  6899  caucvgprprlem2  6900  lttrsr  6939  ltsosr  6941  ltasrg  6947  recexgt0sr  6950  mulgt0sr  6954  aptisr  6955  mulextsr1  6957  srpospr  6959  caucvgsrlemgt1  6971  caucvgsrlemoffres  6976  caucvgsr  6978  axprecex  7046  axpre-ltwlin  7049  axpre-lttrn  7050  axpre-apti  7051  axpre-ltadd  7052  axpre-mulgt0  7053  axpre-mulext  7054  axcaucvglemcau  7064  axcaucvglemres  7065  axcaucvg  7066  ltxrlt  7178  lttri3  7191  ltne  7196  eqle  7202  reapti  7679  apreim  7703  squeeze0  7982  lbreu  8023  lble  8025  suprleubex  8032  nnge1  8062  nn2ge  8071  nn1gt1  8072  nnsub  8077  nominpos  8268  nn0ge0  8313  elnnnn0b  8332  nn0ge2m1nn  8348  zdclt  8425  suprzclex  8445  peano2uz2  8454  peano5uzti  8455  dfuzi  8457  uzind  8458  uzind3  8460  eluz1  8623  uzind4  8676  indstr  8681  supinfneg  8683  infsupneg  8684  indstr2  8696  ublbneg  8698  elrp  8736  mnfltxr  8861  nn0pnfge0  8866  xrltnsym  8868  xrlttr  8870  xrltso  8871  xrlttri3  8872  xrltne  8883  ngtmnft  8885  xrrebnd  8886  z2ge  8893  xltnegi  8902  ixxval  8919  elixx1  8920  elioo2  8944  iccid  8948  iccsupr  8989  repos  8993  fzval  9031  elfz1  9034  fzm1  9117  qbtwnre  9265  qbtwnxr  9266  flval  9276  modqid2  9353  modqmuladdnn0  9370  serige0  9473  expival  9478  expge0  9512  expge1  9513  facdiv  9665  facwordi  9667  ovshftex  9707  shftfibg  9708  shftfib  9711  shftfn  9712  2shfti  9719  sqrt0rlem  9889  resqrexlemex  9911  rsqrmo  9913  resqrtcl  9915  rersqrtthlem  9916  sqrtsq  9930  cau3lem  10000  caubnd2  10003  maxleim  10091  maxabslemval  10094  maxleast  10099  maxleb  10102  fimaxre2  10109  minmax  10112  climi  10126  climeu  10135  climmo  10137  2clim  10140  addcn2  10149  mulcn2  10151  cn1lem  10152  dvdsabsb  10214  0dvds  10215  alzdvds  10254  dvdsext  10255  fzo0dvdseq  10257  2tp1odd  10284  2teven  10287  divalglemnn  10318  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  gcdval  10351  gcddvds  10355  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlemex  10390  bezoutlemeu  10396  bezoutlemsup  10398  dfgcd3  10399  bezout  10400  dvdsgcd  10401  dfgcd2  10403  dvdssq  10420  lcmval  10445  lcmcllem  10449  dvdslcm  10451  lcmledvds  10452  lcmgcdlem  10459  lcmdvds  10461  coprmgcdb  10470  coprmdvds2  10475  cncongr1  10485  cncongr2  10486  isprm  10491  dvdsnprmd  10507  dvdsprm  10518  exprmfct  10519  isprm6  10526  prmexpb  10530  prmfac1  10531  rpexp  10532  sqrt2irr  10541  oddpwdclemdc  10551  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  sqne2sq  10555