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  5931  isorel  5949  isocnv  5952  isotr  5957  isopolem  5963  isosolem  5965  f1oiso  5967  f1oiso2  5968  caovordig  6188  caovordg  6190  caovord  6194  caofrss  6267  caoftrn  6268  poxp  6397  tposoprab  6446  ertr  6717  ecopovsym  6800  ecopovtrn  6801  ecopovsymg  6803  ecopovtrng  6804  th3qlem2  6807  domeng  6923  eqeng  6939  snfig  6989  nneneq  7043  nnfi  7059  ssfilem  7062  ssfilemd  7064  domfiexmid  7067  dif1enen  7069  diffitest  7076  findcard  7077  findcard2  7078  findcard2s  7079  diffisn  7082  tridc  7089  fimax2gtrilemstep  7090  inffiexmid  7098  unsnfi  7111  fiintim  7123  fisseneq  7127  isbth  7166  supmoti  7192  eqsupti  7195  supubti  7198  suplubti  7199  suplub2ti  7200  supmaxti  7203  supsnti  7204  isotilem  7205  isoti  7206  supisolem  7207  supisoex  7208  cardcl  7385  isnumi  7386  cardval3ex  7389  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidapne  7479  nqtri3or  7616  ltsonq  7618  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  nsmallnqq  7632  subhalfnqq  7634  ltbtwnnqq  7635  prarloclemarch2  7639  nqnq0pi  7658  prcdnql  7704  prcunqu  7705  prnminu  7709  genpcdl  7739  genprndl  7741  genprndu  7742  genpdisj  7743  nqprm  7762  nqprrnd  7763  nqprdisj  7764  nqprloc  7765  nqprlu  7767  nqprl  7771  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  1idpru  7811  ltnqpr  7813  ltnqpri  7814  prplnqu  7840  recexprlemelu  7843  recexprlemm  7844  recexprlemloc  7851  recexprlem1ssl  7853  recexprlemss1u  7856  cauappcvgprlemm  7865  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem2  7880  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem2  7900  caucvgprprlemelu  7906  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnbj  7913  caucvgprprlemmu  7915  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlem1  7929  caucvgprprlem2  7930  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexpr  7945  lttrsr  7982  ltsosr  7984  ltasrg  7990  recexgt0sr  7993  mulgt0sr  7998  aptisr  7999  mulextsr1  8001  srpospr  8003  caucvgsrlemgt1  8015  caucvgsrlemoffres  8020  caucvgsr  8022  map2psrprg  8025  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  axprecex  8100  axpre-ltwlin  8103  axpre-lttrn  8104  axpre-apti  8105  axpre-ltadd  8106  axpre-mulgt0  8107  axpre-mulext  8108  axcaucvglemcau  8118  axcaucvglemres  8119  axcaucvg  8120  axpre-suploclemres  8121  axpre-suploc  8122  ltxrlt  8245  lttri3  8259  ltne  8264  eqle  8271  ltordlem  8662  reapti  8759  apreim  8783  squeeze0  9084  lbreu  9125  lble  9127  suprleubex  9134  sup3exmid  9137  nnge1  9166  nn2ge  9176  nn1gt1  9177  nnsub  9182  nominpos  9382  nn0ge0  9427  elnnnn0b  9446  nn0ge2m1nn  9462  zdclt  9557  suprzclex  9578  peano2uz2  9587  peano5uzti  9588  dfuzi  9590  uzind  9591  uzind3  9593  eluz1  9759  uzind4  9822  indstr  9827  supinfneg  9829  infsupneg  9830  infregelbex  9832  indstr2  9843  ublbneg  9847  irrmulap  9882  elpq  9883  elpqb  9884  elrp  9890  mnfltxr  10021  nn0pnfge0  10026  xrltnsym  10028  xrlttr  10030  xrltso  10031  xrlttri3  10032  xrltne  10048  ngtmnft  10052  nmnfgt  10053  xrrebnd  10054  z2ge  10061  xltnegi  10070  xltadd1  10111  xsubge0  10116  xleaddadd  10122  ixxval  10131  elixx1  10132  elioo2  10156  iccid  10160  iccsupr  10201  repos  10205  fzval  10245  elfz1  10248  fzm1  10335  zsupcllemstep  10490  suprzubdc  10497  zsupssdc  10499  qdclt  10506  exbtwnzlemstep  10508  exbtwnzlemex  10510  qbtwnre  10517  qbtwnxr  10518  flval  10533  apbtwnz  10535  modqid2  10614  modqmuladdnn0  10631  exp3val  10804  expge0  10838  expge1  10839  nn0ltexp2  10972  facdiv  11001  facwordi  11003  hashinfom  11041  hashennn  11043  hashunlem  11068  zfz1iso  11106  wrdlen1  11155  fstwrdne0  11157  wrdl1exs1  11210  pfxsuffeqwrdeq  11283  pfxsuff1eqwrdeq  11284  ccats1pfxeq  11299  ccats1pfxeqrex  11300  pfxccatin12lem3  11317  ovshftex  11397  shftfibg  11398  shftfib  11401  shftfn  11402  2shfti  11409  sqrt0rlem  11581  resqrexlemex  11603  rsqrmo  11605  resqrtcl  11607  rersqrtthlem  11608  sqrtsq  11622  cau3lem  11692  caubnd2  11695  maxleim  11783  maxabslemval  11786  maxleast  11791  maxleb  11794  fimaxre2  11805  minmax  11808  xrmaxleim  11822  xrmaxiflemval  11828  xrmaxaddlem  11838  xrminmax  11843  xrbdtri  11854  climi  11865  climeu  11874  climmo  11876  2clim  11879  addcn2  11888  mulcn2  11890  reccn2ap  11891  cn1lem  11892  summodc  11962  zsumdc  11963  fsum3  11966  cvgratz  12111  ntrivcvgap0  12128  prodmodc  12157  zproddc  12158  fprodseq  12162  fprodntrivap  12163  sinltxirr  12340  dvdsabsb  12389  0dvds  12390  alzdvds  12433  dvdsext  12434  fzo0dvdseq  12436  2tp1odd  12463  2teven  12466  divalglemnn  12497  divalglemeunn  12500  divalglemeuneg  12502  bitsinv1lem  12540  gcdval  12548  gcddvds  12552  bezoutlemstep  12586  bezoutlemmain  12587  bezoutlemex  12590  bezoutlemeu  12596  bezoutlemsup  12598  dfgcd3  12599  bezout  12600  dvdsgcd  12601  dfgcd2  12603  dvdssq  12620  uzwodc  12626  nnwofdc  12627  lcmval  12653  lcmcllem  12657  dvdslcm  12659  lcmledvds  12660  lcmgcdlem  12667  lcmdvds  12669  coprmgcdb  12678  coprmdvds2  12683  cncongr1  12693  cncongr2  12694  isprm  12699  dvdsnprmd  12715  dvdsprm  12727  exprmfct  12728  isprm6  12737  prmexpb  12741  prmfac1  12742  rpexp  12743  sqrt2irr  12752  oddpwdclemdc  12763  oddpwdc  12764  sqpweven  12765  2sqpwodd  12766  sqne2sq  12767  nnoddn2prmb  12853  pceu  12886  pczpre  12888  pcdiv  12893  pcdvdsb  12911  difsqpwdvds  12929  pcmpt  12934  pcmptdvds  12936  oddprmdvds  12945  prmpwdvds  12946  infpnlem2  12951  oddennn  13031  evenennn  13032  exmidunben  13065  nninfdclemcl  13087  nninfdclemp1  13089  nninfdc  13092  infpn2  13095  eqgen  13832  zndvds  14682  znleval  14686  comet  15242  metcnpi  15258  metcnpi2  15259  metcnpi3  15260  addcncntoplem  15304  cncfi  15321  elcncf1di  15322  mulcncflem  15350  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeulemeu  15365  dedekindeu  15366  suplociccreex  15367  suplociccex  15368  dedekindicclemuub  15369  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemeu  15374  dedekindicclemicc  15375  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemlr  15380  ivthinclemuopn  15381  ivthinclemur  15382  ivthinclemloc  15384  ivthinc  15386  ivthreinc  15388  dich0  15395  ivthdich  15396  limcimo  15408  cnplimclemr  15412  limccnp2lem  15419  limccoap  15421  eldvap  15425  logltb  15617  lgsdir  15783  lgsne0  15786  gausslemma2dlem0i  15805  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  2lgslem2  15840  2lgs  15852  2sqlem6  15868  2sqlem8  15871  2sqlem10  15873  lfgredg2dom  16002  istrl  16255  clwwlkn0  16278  clwwlkext2edg  16292  clwwlknonccat  16303  clwwlknonex2  16309  iseupth  16317  konigsberg  16363  sbthom  16681  trilpo  16698  trirec0  16699  apdiff  16703  reap0  16714  cndcap  16715  nconstwlpolem  16721  neapmkv  16724  neap0mkv  16725  ltlenmkv  16726