Theorem eqeq1 1890

Description: Equality implies equivalence of equalities.

Assertion

Ref	Expression
eqeq1	|- (A = B -> (A = C <-> B = C))

Proof of Theorem eqeq1

Step	Hyp	Ref	Expression
1		dfcleq 1878	. . . . . 6 |- (A = B <-> A.x(x e. A <-> x e. B))
2	1	biimpi 168	. . . . 5 |- (A = B -> A.x(x e. A <-> x e. B))
3	2	19.21bi 1408	. . . 4 |- (A = B -> (x e. A <-> x e. B))
4	3	bibi1d 681	. . 3 |- (A = B -> ((x e. A <-> x e. C) <-> (x e. B <-> x e. C)))
5	4	albidv 1656	. 2 |- (A = B -> (A.x(x e. A <-> x e. C) <-> A.x(x e. B <-> x e. C)))
6		dfcleq 1878	. 2 |- (A = C <-> A.x(x e. A <-> x e. C))
7		dfcleq 1878	. 2 |- (B = C <-> A.x(x e. B <-> x e. C))
8	5, 6, 7	3bitr4g 614	1 |- (A = B -> (A = C <-> B = C))

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300

This theorem is referenced by:  eqeq1i 1891  eqeq1d 1892  eqeq2 1893  eqeq12 1896  eqtr 1904  eqsb3lem 1987  eqsb3lemOLD 1988  clelab 2013  neeq1 2024  pm13.18 2085  vtoclgf 2345  cla4gf 2361  cla4gfOLD 2363  eqvincOLD 2388  eqvincf 2389  eueq 2427  moi 2436  euind 2439  reu6 2443  reu7 2447  reuind 2450  sbhypf 2452  eqsbc3 2494  sbceqal 2502  uniiunlem 2693  snjust 3047  elprg 3060  elsncg 3063  intab 3247  uniintsn 3253  dfiun2gOLD 3284  dfiin2g 3286  dfiin2OLD 3288  opth 3532  opthgg 3534  copsexg 3537  copsexgOLD 3538  elopab 3559  solin 3612  limeqOLD 3670  snnex 3801  uniuni 3806  eualeq 3823  eualeqhb 3824  euexeqOLD 3826  euexaleq 3827  eufromeq1 3828  eufromeq2 3829  eufromeq3 3830  eufromeq5 3832  eufromeq6 3833  euobj1 3834  orduninsuc 3925  opbrop 4064  relop 4113  ideqg 4114  ideqgOLD 4115  funopg 4454  funcnvuni 4482  iunfopabOLD 4543  dffn5 4717  fvelrnb 4719  fvopab4g 4742  fvopabn 4749  eqfnfv 4766  abrexexlem2 4835  funiunfv 4842  dff13f 4851  f1fveq 4852  isowe 4880  f1oiso 4881  f1oweALT 4883  eloprabg 4936  oprabval2gf 4955  oprabval3 4959  oprabval6g 4962  oprvelrn 4969  caoprcan 4988  fparlem1 5081  fparlem2 5082  fparlem3 5083  fparlem4 5084  fsplit 5086  onopriun 5118  tz7.44-1 5136  tz7.44-2 5137  tz7.44-3 5138  rdglem2 5146  oev 5198  oalimcl 5242  omlimcl 5257  odi 5258  nneob 5312  elqs 5348  elqsi 5349  brecop 5365  eceqopreq 5372  th3qlem1 5373  th3q 5376  2dom 5486  fundmen 5487  pw2en 5505  ac6sfilem3 5508  xpmapenlem4 5593  nneneq 5606  abfii3 5653  abfii4 5654  ordtype 5691  hartoglem 5692  hartog 5693  tz9.12lem1 5770  tz9.12lem3 5772  scott0 5847  omsubsuc 5877  omsublim 5887  aceq3lem 5894  aceq5lem3 5899  aceq5lem4 5900  aceq6b 5904  ac6 5917  kmlem9 5935  kmlem12 5938  brdom7disj 5966  brdom6disj 5967  card1 5983  unxpdomlem 5995  cardiun 6011  alephval3 6051  cardcf 6059  cfeq0 6062  cfsuc 6063  ltsopq 6227  genpv 6254  genpelv 6255  genpprecl 6256  genpnnp 6260  prlem934b 6290  ltsosr 6355  ltresr 6410  ltsor 6413  axcnre 6439  addcan 6507  neg11 6569  lesub0 6867  mulcant2i 6879  mul0or 6884  div11 6941  rec11i 6954  eqneg 6983  nnleltp1 7138  elz 7346  nn0ind-raph 7426  elq 7437  fseqsupcl 7704  fseqsupubi 7705  seq1suclem 7729  expval 7813  sq11 7874  sqeqor 7895  nn0opth2 7918  sqrlem21 7943  sqrlem22 7944  sqr00 7964  cru 7988  reval 8005  imval 8006  abs00 8104  sumeq1 8242  climuni 8359  infcvgaux1i 8480  infcvgaux2i 8481  infcvglem1 8482  ef1tlubi 8644  reef11 8674  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  ruclem12 8790  infxpidmlem2 8822  eltopsp 8873  tpsex 8874  istps 8875  eltg3 8896  subbas 8914  subbas2 8915  subtop 8916  fctop 8920  cctop 8922  txbas 8933  txuni 8935  meteq0 9089  dscmet 9196  gxval 9381  gxdi 9422  nvz 9629  vacnlem6 9672  nmosetn0 9767  nmolb 9773  nmoubi 9774  nmlno0lem 9793  nmlno0i 9794  minveclem10 9899  minveclem14 9903  minvecex 9923  spwval2 9996  cosh111 10071  efghgrpilem 10073  efifolem3 10078  circgrp 10094  findcardOLD 10179  spfi 10217  fiiu2 10220  tx1cn 10223  tx2cn 10224  uptx 10226  issubsp 10245  subtopmet 10256  fipfil2 10272  fsubbas 10281  fbunfip 10282  filrn 10293  limfil 10297  hausfillim 10303  isfilmap 10308  filmapss 10309  elfilmap 10312  sflimf 10318  cncomp 10331  ismgm 10367  hvsubeq0 10567  hvaddcan 10569  normsub0 10636  hlimunii 10742  norm1exi 10755  projlem8 10826  projlem10 10828  projlem13 10831  projlem15 10833  pjth 10867  pjval 10872  omlsii 10878  omlsi 10879  pjoml 10902  shsel 10911  h1de2ci 11112  spansneleq 11126  h1datomi 11137  h1datom 11138  spansncv 11233  5oalem6 11239  pj11 11294  nmopsetn0 11429  nmfnsetn0 11442  nmoplb 11468  nmopub 11469  nmfnlb 11485  nmfnleub 11486  nmlnop0iALT 11557  nmlnop0 11560  lnopeq 11571  nmopun 11576  nmcopexlem1 11588  lnopconi 11600  nmcfnexlem1 11617  lnfnconi 11627  branmfn 11675  branmfnOLD 11676  pjnmopi 11719  pj3i 11781  atss 11918  atom1d 11925  irred 11967  cdj3lem2 12007  bnj135 12467  bnj142 12474  bnj1468 13145  bnj1483 13160  fz1eqblem 13608  fz1eqb 13609  ghomf1olem 13637  divalg 13706  ndvdssub 13710  gcdval 13715  mulgcdlem2 13757  coprm 13782  sneqrg 13822  mpt2fun 13843  frxp 13951  sltval2 13997  sltintdifex 14004  axfelem12 14042  axfelem16 14046  brtxp 14067  elaltxp 14098  elo 14342  fiiu 14344  eloi 14400  cmprelid2 14447  cnveq2 14455  repfuntw 14502  cbcpcp 14504  cbicplem 14508  iscst3 14521  ismxl2 14609  prodeq1 14658  dffprod 14670  grpdrcan 14738  ununr 14769  bsi 14845  hmeogrp 14892  homcard 14893  subspemp 14903  efilcp 14922  fisub 14924  rcfpfillem1 14928  rcfpfillem3 14930  rcfpfillem6 14933  rcfpfil 14934  cnpfillim4 14947  cntrset 15000  iint 15012  trnij 15015  cnvtr 15016  mamb 15030  ismonb2 15161  cmpmon 15164  isepib2 15171  vtarsuelt 15272  partarelt2 15274  subtr 15352  subtr2 15353  dfiin2gOLD 15356  fictblem 15370  fictb 15371  inficlALT 15372  ordtypeOLD 15382  hartoglemOLD 15383  hartogOLD 15384  omsubsucOLD 15386  omsublimOLD 15396  opncldf1 15402  opncldf2 15403  opncldf3 15404  compsublem 15430  compsub 15431  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem3 15439  cnconn 15444  fneuni 15485  comppfsc 15517  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  fbasfip 15556  ufileu 15573  ufilen 15579  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  sfcls 15604  filclus 15605  fcluscnplem 15617  fcluscomplem 15620  ufcomp 15622  sfclusf 15624  tailf 15633  istail 15634  filnetlem1 15640  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  filnet 15645  unirep 15664  prfunOLD 15677  foelrn 15685  foco2 15686  f1opr 15714  eropreu 15733  eroprv 15734  add20 15777  sdclem1 15809  fdc 15812  txsubsp 15912  txopn 15913  txmet 15925  sstotbnd 15936  totbndss 15937  totbndbnd 15944  heiborlem1 15955  heiborlem8 15962  heiborlem11 15965  heiborlem30 15984  bfplem3 16000  rrntotbndlem1 16020  rrntotbnd 16022  phtpyval 16047  elpi1 16089  maxidlmax 16191  prnc 16215  isfldidl 16216  dmnnzd 16223  erdisj3 16266  elqs2 16267  prter3 16286  pm13.18OLD 16371  pm13.183 16373  pm13.192 16374  isseta 16405  equncomVD 16692  poslem 16774  atomnle 17016  glbconx 17029  isline 17220  ispoint 17223  pmapglbx 17251  ispsubcl2 17356

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain