Theorem breq2 3993

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348   ∈ wcel 2141  ⟨cop 3586   class class class wbr 3989

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-un 3125  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990

This theorem is referenced by:  breq12  3994  breq2i  3997  breq2d  4001  nbrne1  4008  brralrspcev  4047  brimralrspcev  4048  pocl  4288  swopolem  4290  swopo  4291  sowlin  4305  sotricim  4308  sotritrieq  4310  seex  4320  frind  4337  wetriext  4561  vtoclr  4659  posng  4683  brcog  4778  brcogw  4780  opelcnvg  4791  dfdmf  4804  breldmg  4817  dfrnf  4852  dmcoss  4880  resieq  4901  dfres2  4943  elimag  4957  elreimasng  4977  elimasn  4978  intirr  4997  poirr2  5003  poltletr  5011  dffun6f  5211  dffun4f  5214  fun11  5265  brprcneu  5489  fv3  5519  tz6.12c  5526  relelfvdm  5528  funbrfv  5535  fnbrfvb  5537  funfvdm2f  5561  fndmdif  5601  dff3im  5641  fmptco  5662  foeqcnvco  5769  isorel  5787  isocnv  5790  isotr  5795  isopolem  5801  isosolem  5803  f1oiso  5805  f1oiso2  5806  caovordig  6018  caovordg  6020  caovord  6024  caofrss  6085  caoftrn  6086  poxp  6211  tposoprab  6259  ertr  6528  ecopovsym  6609  ecopovtrn  6610  ecopovsymg  6612  ecopovtrng  6613  th3qlem2  6616  domeng  6730  eqeng  6744  snfig  6792  nneneq  6835  nnfi  6850  ssfilem  6853  domfiexmid  6856  dif1enen  6858  diffitest  6865  findcard  6866  findcard2  6867  findcard2s  6868  diffisn  6871  tridc  6877  fimax2gtrilemstep  6878  inffiexmid  6884  unsnfi  6896  fiintim  6906  fisseneq  6909  isbth  6944  supmoti  6970  eqsupti  6973  supubti  6976  suplubti  6977  suplub2ti  6978  supmaxti  6981  supsnti  6982  isotilem  6983  isoti  6984  supisolem  6985  supisoex  6986  cardcl  7158  isnumi  7159  cardval3ex  7162  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  nqtri3or  7358  ltsonq  7360  ltanqg  7362  ltmnqg  7363  ltexnqq  7370  nsmallnqq  7374  subhalfnqq  7376  ltbtwnnqq  7377  prarloclemarch2  7381  nqnq0pi  7400  prcdnql  7446  prcunqu  7447  prnminu  7451  genpcdl  7481  genprndl  7483  genprndu  7484  genpdisj  7485  nqprm  7504  nqprrnd  7505  nqprdisj  7506  nqprloc  7507  nqprlu  7509  nqprl  7513  addnqprlemru  7520  addnqprlemfl  7521  addnqprlemfu  7522  mulnqprlemru  7536  mulnqprlemfl  7537  mulnqprlemfu  7538  1idpru  7553  ltnqpr  7555  ltnqpri  7556  prplnqu  7582  recexprlemelu  7585  recexprlemm  7586  recexprlemloc  7593  recexprlem1ssl  7595  recexprlemss1u  7598  cauappcvgprlemm  7607  cauappcvgprlemopu  7610  cauappcvgprlemupu  7611  cauappcvgprlemdisj  7613  cauappcvgprlemloc  7614  cauappcvgprlemladdfu  7616  cauappcvgprlemladdru  7618  cauappcvgprlemladdrl  7619  cauappcvgprlem2  7622  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemopu  7633  caucvgprlemupu  7634  caucvgprlemdisj  7636  caucvgprlemloc  7637  caucvgprlemcl  7638  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprlem2  7642  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnbj  7655  caucvgprprlemmu  7657  caucvgprprlemexbt  7668  caucvgprprlemaddq  7670  caucvgprprlem1  7671  caucvgprprlem2  7672  suplocexprlemmu  7680  suplocexprlemru  7681  suplocexprlemdisj  7682  suplocexprlemloc  7683  suplocexprlemub  7685  suplocexpr  7687  lttrsr  7724  ltsosr  7726  ltasrg  7732  recexgt0sr  7735  mulgt0sr  7740  aptisr  7741  mulextsr1  7743  srpospr  7745  caucvgsrlemgt1  7757  caucvgsrlemoffres  7762  caucvgsr  7764  map2psrprg  7767  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axprecex  7842  axpre-ltwlin  7845  axpre-lttrn  7846  axpre-apti  7847  axpre-ltadd  7848  axpre-mulgt0  7849  axpre-mulext  7850  axcaucvglemcau  7860  axcaucvglemres  7861  axcaucvg  7862  axpre-suploclemres  7863  axpre-suploc  7864  ltxrlt  7985  lttri3  7999  ltne  8004  eqle  8011  ltordlem  8401  reapti  8498  apreim  8522  squeeze0  8820  lbreu  8861  lble  8863  suprleubex  8870  sup3exmid  8873  nnge1  8901  nn2ge  8911  nn1gt1  8912  nnsub  8917  nominpos  9115  nn0ge0  9160  elnnnn0b  9179  nn0ge2m1nn  9195  zdclt  9289  suprzclex  9310  peano2uz2  9319  peano5uzti  9320  dfuzi  9322  uzind  9323  uzind3  9325  eluz1  9491  uzind4  9547  indstr  9552  supinfneg  9554  infsupneg  9555  infregelbex  9557  indstr2  9568  ublbneg  9572  elpq  9607  elpqb  9608  elrp  9612  mnfltxr  9743  nn0pnfge0  9748  xrltnsym  9750  xrlttr  9752  xrltso  9753  xrlttri3  9754  xrltne  9770  ngtmnft  9774  nmnfgt  9775  xrrebnd  9776  z2ge  9783  xltnegi  9792  xltadd1  9833  xsubge0  9838  xleaddadd  9844  ixxval  9853  elixx1  9854  elioo2  9878  iccid  9882  iccsupr  9923  repos  9927  fzval  9967  elfz1  9970  fzm1  10056  exbtwnzlemstep  10204  exbtwnzlemex  10206  qbtwnre  10213  qbtwnxr  10214  flval  10228  apbtwnz  10230  modqid2  10307  modqmuladdnn0  10324  exp3val  10478  expge0  10512  expge1  10513  nn0ltexp2  10644  facdiv  10672  facwordi  10674  hashinfom  10712  hashennn  10714  hashunlem  10739  zfz1iso  10776  ovshftex  10783  shftfibg  10784  shftfib  10787  shftfn  10788  2shfti  10795  sqrt0rlem  10967  resqrexlemex  10989  rsqrmo  10991  resqrtcl  10993  rersqrtthlem  10994  sqrtsq  11008  cau3lem  11078  caubnd2  11081  maxleim  11169  maxabslemval  11172  maxleast  11177  maxleb  11180  fimaxre2  11190  minmax  11193  xrmaxleim  11207  xrmaxiflemval  11213  xrmaxaddlem  11223  xrminmax  11228  xrbdtri  11239  climi  11250  climeu  11259  climmo  11261  2clim  11264  addcn2  11273  mulcn2  11275  reccn2ap  11276  cn1lem  11277  summodc  11346  zsumdc  11347  fsum3  11350  cvgratz  11495  ntrivcvgap0  11512  prodmodc  11541  zproddc  11542  fprodseq  11546  fprodntrivap  11547  dvdsabsb  11772  0dvds  11773  alzdvds  11814  dvdsext  11815  fzo0dvdseq  11817  2tp1odd  11843  2teven  11846  divalglemnn  11877  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  suprzubdc  11907  zsupssdc  11909  gcdval  11914  gcddvds  11918  bezoutlemstep  11952  bezoutlemmain  11953  bezoutlemex  11956  bezoutlemeu  11962  bezoutlemsup  11964  dfgcd3  11965  bezout  11966  dvdsgcd  11967  dfgcd2  11969  dvdssq  11986  uzwodc  11992  nnwofdc  11993  lcmval  12017  lcmcllem  12021  dvdslcm  12023  lcmledvds  12024  lcmgcdlem  12031  lcmdvds  12033  coprmgcdb  12042  coprmdvds2  12047  cncongr1  12057  cncongr2  12058  isprm  12063  dvdsnprmd  12079  dvdsprm  12091  exprmfct  12092  isprm6  12101  prmexpb  12105  prmfac1  12106  rpexp  12107  sqrt2irr  12116  oddpwdclemdc  12127  oddpwdc  12128  sqpweven  12129  2sqpwodd  12130  sqne2sq  12131  nnoddn2prmb  12216  pceu  12249  pczpre  12251  pcdiv  12256  pcdvdsb  12273  difsqpwdvds  12291  pcmpt  12295  pcmptdvds  12297  oddprmdvds  12306  prmpwdvds  12307  infpnlem2  12312  oddennn  12347  evenennn  12348  exmidunben  12381  nninfdclemcl  12403  nninfdclemp1  12405  nninfdc  12408  infpn2  12411  comet  13293  metcnpi  13309  metcnpi2  13310  metcnpi3  13311  addcncntoplem  13345  cncfi  13359  elcncf1di  13360  mulcncflem  13384  dedekindeulemuub  13389  dedekindeulemloc  13391  dedekindeulemlu  13393  dedekindeulemeu  13394  dedekindeu  13395  suplociccreex  13396  suplociccex  13397  dedekindicclemuub  13398  dedekindicclemloc  13400  dedekindicclemlu  13402  dedekindicclemeu  13403  dedekindicclemicc  13404  dedekindicc  13405  ivthinclemlopn  13408  ivthinclemlr  13409  ivthinclemuopn  13410  ivthinclemur  13411  ivthinclemloc  13413  ivthinc  13415  limcimo  13428  cnplimclemr  13432  limccnp2lem  13439  limccoap  13441  eldvap  13445  logltb  13589  lgsdir  13730  lgsne0  13733  2sqlem6  13750  2sqlem8  13753  2sqlem10  13755  sbthom  14058  trilpo  14075  trirec0  14076  apdiff  14080  reap0  14090  nconstwlpolem  14096  neapmkv  14099