Theorem eqeq1 2241

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq1	⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Proof of Theorem eqeq1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2228	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1607	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 233	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1873	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2228	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2228	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396   = wceq 1398   ∈ wcel 2205

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-5 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-cleq 2227

This theorem is referenced by:  eqeq1i  2242  eqeq1d  2243  eqeq2  2244  eqeq12  2247  eqtr  2252  eqsb1lem  2337  clelab  2362  neeq1  2427  pm13.18  2495  issetf  2823  sbhypf  2866  vtoclgft  2867  eqvincf  2945  pm13.183  2958  eueq  2991  mob  3002  euind  3007  reuind  3025  eqsbc1  3085  csbhypf  3180  uniiunlem  3332  snjust  3699  elsng  3709  elprg  3714  rabrsndc  3764  sneqrg  3871  preq12bg  3882  intab  3983  dfiin2g  4029  exmidsssnc  4321  exmid1stab  4326  opthg  4359  copsexg  4365  euotd  4376  elopab  4381  snnex  4574  uniuni  4577  eusv1  4578  reusv3  4586  ordtriexmid  4648  ontriexmidim  4649  onsucelsucexmidlem1  4655  onsucelsucexmid  4657  regexmidlemm  4659  regexmidlem1  4660  reg2exmidlema  4661  wetriext  4704  nn0suc  4731  nndceq0  4745  0elnn  4746  elxpi  4770  opbrop  4834  relop  4910  ideqg  4911  elrnmpt  5011  elrnmpt1  5013  elrnmptg  5014  restidsing  5099  cnveqb  5223  relcoi1  5299  funopg  5391  funcnvuni  5430  f0rn0  5567  fun11iun  5640  fvelrnb  5729  fvmptg  5758  fndmin  5790  eldmrexrn  5823  fmptco  5848  foco2  5932  elabrex  5936  elabrexg  5937  abrexco  5938  f1veqaeq  5948  f1oiso  6005  eusvobj2  6044  acexmidlema  6049  acexmidlemb  6050  acexmidlem2  6055  acexmidlemv  6056  oprabid  6090  mpofun  6163  elrnmpog  6174  elrnmpo  6175  ralrnmpo  6176  rexrnmpo  6177  ovi3  6199  ov6g  6200  ovelrn  6211  caovcang  6224  caovcan  6227  elabreximd  6329  eloprabi  6405  funsssuppss  6471  suppssrst  6474  suppssrgst  6475  dftpos4  6507  tfr1onlemaccex  6592  tfrcllemaccex  6605  elqsg  6832  qsel  6859  brecop  6872  eroveu  6873  erovlem  6874  th3qlem1  6884  th3q  6887  elixpsn  6983  ixpsnf1o  6984  2dom  7059  fundmen  7060  xpf1o  7110  nneneq  7124  tridc  7170  elssdc  7175  eqsndc  7176  prfidceq  7201  tpfidceq  7203  fisseneq  7208  fidcenumlemrks  7236  elfi  7271  supsnti  7309  isotilem  7310  updjudhcoinrg  7385  updjud  7386  omp1eom  7399  difinfsn  7404  ctmlemr  7412  ismkvnex  7459  omniwomnimkv  7471  nninfwlpoimlemginf  7480  nninfwlpoimlemdc  7481  nninfinfwlpolem  7482  exmidaclem  7528  exmidac  7529  onntri35  7560  exmidapne  7590  indpi  7673  nqtri3or  7727  enq0sym  7763  enq0ref  7764  enq0tr  7765  enq0breq  7767  addnq0mo  7778  mulnq0mo  7779  mulnnnq0  7781  genipv  7840  genpelvl  7843  genpelvu  7844  addsrmo  8074  mulsrmo  8075  aptisr  8110  ltresr  8170  axcnre  8212  axpre-apti  8216  ltordlem  8773  apreap  8878  apreim  8894  aprcl  8937  aptap  8941  sup3exmid  9248  creur  9250  creui  9251  nn1m1nn  9272  nn1gt1  9288  elz  9596  nn0ind-raph  9713  nltpnft  10166  xnegeq  10179  xrpnfdc  10194  xrmnfdc  10195  xleaddadd  10239  flqeqceilz  10704  1tonninf  10827  iseqf1olemqval  10886  iseqf1olemqk  10893  seq3f1olemqsum  10899  exp3val  10927  wrd2ind  11440  shftfvalg  11528  shftfval  11531  summodc  12094  fsum3  12098  telfsumo  12177  mertenslemub  12245  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  prodmodc  12289  fprodseq  12294  fprodcl2lem  12316  ndvdssub  12641  gcdval  12680  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  lcmval  12785  coprmgcdb  12810  coprmdvds1  12813  divgcdcoprmex  12824  dvdsprime  12844  nprm  12845  dvdsprm  12859  coprm  12866  qnumval  12907  qdenval  12908  m1dvdsndvds  12971  reumodprminv  12976  pceu  13018  pcval  13019  pczpre  13020  pcdiv  13025  4sqlem2  13112  4sqlem4  13115  4sqlemafi  13118  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  4sqlem12  13125  4sq  13133  ballotfilem2  13172  ennnfonelemj0  13236  ennnfonelemjn  13237  ennnfonelem0  13240  ennnfonelemp1  13241  ennnfonelemnn0  13257  ennnfonelemim  13259  unct  13277  gsum0g  13659  gsumval2  13660  ghmf1  14026  gfsumval  14102  rrgeq0i  14510  domneq0  14519  lss1d  14657  lspsn  14690  ellspsn  14691  znf1o  14925  znidom  14931  znunit  14933  istopon  15004  toponsspwpwg  15013  epttop  15081  txuni2  15247  xmeteq0  15350  comet  15490  elply  15725  elply2  15726  mpodvdsmulf1o  15984  perfectlem2  15994  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  gausslemma2dlem0i  16056  2lgslem1b  16088  2lgslem3  16100  2sqlem2  16114  2sqlem8  16122  2sqlem9  16123  upgredg2vtx  16269  uspgredg2v  16342  ushgredgedgloop  16349  vtxduspgrfvedgfi  16422  1loopgrvd2fi  16426  wlkeq  16475  depindlem1  16627  bj-charfunbi  16707  bj-nn0suc0  16846  bj-inf2vnlem1  16866  bj-inf2vnlem2  16867  bj-nn0sucALT  16874  subctctexmid  16900  pw1nct  16903  exmidnotnotr  16905  exmidcon  16906  exmidpeirce  16907  nnsf  16909  peano3nninf  16911  nninfall  16913  exmidsbthr  16929  trilpo  16953  trirec0  16954  redcwlpo  16966  redc0  16968  dceqnconst  16972