Theorem eqeq1 2184

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 2171	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1558	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 233	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1824	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2171	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2171	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351   = wceq 1353   ∈ wcel 2148

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqeq1i  2185  eqeq1d  2186  eqeq2  2187  eqeq12  2190  eqtr  2195  eqsb1lem  2280  clelab  2303  neeq1  2360  pm13.18  2428  issetf  2745  sbhypf  2787  vtoclgft  2788  eqvincf  2863  pm13.183  2876  eueq  2909  mob  2920  euind  2925  reuind  2943  eqsbc1  3003  csbhypf  3096  uniiunlem  3245  snjust  3598  elsng  3608  elprg  3613  rabrsndc  3661  sneqrg  3763  preq12bg  3774  intab  3874  dfiin2g  3920  exmidsssnc  4204  exmid1stab  4209  opthg  4239  copsexg  4245  euotd  4255  elopab  4259  snnex  4449  uniuni  4452  eusv1  4453  reusv3  4461  ordtriexmid  4521  ontriexmidim  4522  onsucelsucexmidlem1  4528  onsucelsucexmid  4530  regexmidlemm  4532  regexmidlem1  4533  reg2exmidlema  4534  wetriext  4577  nn0suc  4604  nndceq0  4618  0elnn  4619  elxpi  4643  opbrop  4706  relop  4778  ideqg  4779  elrnmpt  4877  elrnmpt1  4879  elrnmptg  4880  restidsing  4964  cnveqb  5085  relcoi1  5161  funopg  5251  funcnvuni  5286  f0rn0  5411  fun11iun  5483  fvelrnb  5564  fvmptg  5593  fndmin  5624  eldmrexrn  5658  fmptco  5683  foco2  5755  elabrex  5759  abrexco  5760  f1veqaeq  5770  f1oiso  5827  eusvobj2  5861  acexmidlema  5866  acexmidlemb  5867  acexmidlem2  5872  acexmidlemv  5873  oprabid  5907  mpofun  5977  elrnmpog  5987  elrnmpo  5988  ralrnmpo  5989  rexrnmpo  5990  ovi3  6011  ov6g  6012  ovelrn  6023  caovcang  6036  caovcan  6039  eloprabi  6197  dftpos4  6264  tfr1onlemaccex  6349  tfrcllemaccex  6362  elqsg  6585  qsel  6612  brecop  6625  eroveu  6626  erovlem  6627  th3qlem1  6637  th3q  6640  elixpsn  6735  ixpsnf1o  6736  2dom  6805  fundmen  6806  xpf1o  6844  nneneq  6857  tridc  6899  fisseneq  6931  fidcenumlemrks  6952  elfi  6970  supsnti  7004  isotilem  7005  updjudhcoinrg  7080  updjud  7081  omp1eom  7094  difinfsn  7099  ctmlemr  7107  ismkvnex  7153  omniwomnimkv  7165  nninfwlpoimlemginf  7174  nninfwlpoimlemdc  7175  exmidaclem  7207  exmidac  7208  onntri35  7236  exmidapne  7259  indpi  7341  nqtri3or  7395  enq0sym  7431  enq0ref  7432  enq0tr  7433  enq0breq  7435  addnq0mo  7446  mulnq0mo  7447  mulnnnq0  7449  genipv  7508  genpelvl  7511  genpelvu  7512  addsrmo  7742  mulsrmo  7743  aptisr  7778  ltresr  7838  axcnre  7880  axpre-apti  7884  ltordlem  8439  apreap  8544  apreim  8560  aprcl  8603  aptap  8607  sup3exmid  8914  creur  8916  creui  8917  nn1m1nn  8937  nn1gt1  8953  elz  9255  nn0ind-raph  9370  nltpnft  9814  xnegeq  9827  xrpnfdc  9842  xrmnfdc  9843  xleaddadd  9887  flqeqceilz  10318  1tonninf  10440  iseqf1olemqval  10487  iseqf1olemqk  10494  seq3f1olemqsum  10500  exp3val  10522  shftfvalg  10827  shftfval  10830  summodc  11391  fsum3  11395  telfsumo  11474  mertenslemub  11542  mertenslemi1  11543  mertenslem2  11544  mertensabs  11545  prodmodc  11586  fprodseq  11591  fprodcl2lem  11613  ndvdssub  11935  gcdval  11960  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  lcmval  12063  coprmgcdb  12088  coprmdvds1  12091  divgcdcoprmex  12102  dvdsprime  12122  nprm  12123  dvdsprm  12137  coprm  12144  qnumval  12185  qdenval  12186  m1dvdsndvds  12248  reumodprminv  12253  pceu  12295  pcval  12296  pczpre  12297  pcdiv  12302  4sqlem2  12387  4sqlem4  12390  ennnfonelemj0  12402  ennnfonelemjn  12403  ennnfonelem0  12406  ennnfonelemp1  12407  ennnfonelemnn0  12423  ennnfonelemim  12425  unct  12443  istopon  13516  toponsspwpwg  13525  epttop  13593  txuni2  13759  xmeteq0  13862  comet  14002  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  2sqlem2  14465  2sqlem8  14473  2sqlem9  14474  bj-charfunbi  14566  bj-nn0suc0  14705  bj-inf2vnlem1  14725  bj-inf2vnlem2  14726  bj-nn0sucALT  14733  subctctexmid  14753  pw1nct  14755  nnsf  14757  peano3nninf  14759  nninfall  14761  exmidsbthr  14774  trilpo  14794  trirec0  14795  redcwlpo  14806  redc0  14808  dceqnconst  14810