Theorem eqeq1 2213

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1371   = wceq 1373   ∈ wcel 2177

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqeq1i  2214  eqeq1d  2215  eqeq2  2216  eqeq12  2219  eqtr  2224  eqsb1lem  2309  clelab  2332  neeq1  2390  pm13.18  2458  issetf  2781  sbhypf  2824  vtoclgft  2825  eqvincf  2902  pm13.183  2915  eueq  2948  mob  2959  euind  2964  reuind  2982  eqsbc1  3042  csbhypf  3136  uniiunlem  3286  snjust  3643  elsng  3653  elprg  3658  rabrsndc  3706  sneqrg  3809  preq12bg  3820  intab  3920  dfiin2g  3966  exmidsssnc  4255  exmid1stab  4260  opthg  4290  copsexg  4296  euotd  4307  elopab  4312  snnex  4503  uniuni  4506  eusv1  4507  reusv3  4515  ordtriexmid  4577  ontriexmidim  4578  onsucelsucexmidlem1  4584  onsucelsucexmid  4586  regexmidlemm  4588  regexmidlem1  4589  reg2exmidlema  4590  wetriext  4633  nn0suc  4660  nndceq0  4674  0elnn  4675  elxpi  4699  opbrop  4762  relop  4836  ideqg  4837  elrnmpt  4936  elrnmpt1  4938  elrnmptg  4939  restidsing  5024  cnveqb  5147  relcoi1  5223  funopg  5314  funcnvuni  5352  f0rn0  5482  fun11iun  5555  fvelrnb  5639  fvmptg  5668  fndmin  5700  eldmrexrn  5734  fmptco  5759  foco2  5835  elabrex  5839  elabrexg  5840  abrexco  5841  f1veqaeq  5851  f1oiso  5908  eusvobj2  5943  acexmidlema  5948  acexmidlemb  5949  acexmidlem2  5954  acexmidlemv  5955  oprabid  5989  mpofun  6060  elrnmpog  6071  elrnmpo  6072  ralrnmpo  6073  rexrnmpo  6074  ovi3  6096  ov6g  6097  ovelrn  6108  caovcang  6121  caovcan  6124  eloprabi  6295  dftpos4  6362  tfr1onlemaccex  6447  tfrcllemaccex  6460  elqsg  6685  qsel  6712  brecop  6725  eroveu  6726  erovlem  6727  th3qlem1  6737  th3q  6740  elixpsn  6835  ixpsnf1o  6836  2dom  6911  fundmen  6912  xpf1o  6956  nneneq  6969  tridc  7011  prfidceq  7040  tpfidceq  7042  fisseneq  7046  fidcenumlemrks  7070  elfi  7088  supsnti  7122  isotilem  7123  updjudhcoinrg  7198  updjud  7199  omp1eom  7212  difinfsn  7217  ctmlemr  7225  ismkvnex  7272  omniwomnimkv  7284  nninfwlpoimlemginf  7293  nninfwlpoimlemdc  7294  nninfinfwlpolem  7295  exmidaclem  7336  exmidac  7337  onntri35  7368  exmidapne  7392  indpi  7475  nqtri3or  7529  enq0sym  7565  enq0ref  7566  enq0tr  7567  enq0breq  7569  addnq0mo  7580  mulnq0mo  7581  mulnnnq0  7583  genipv  7642  genpelvl  7645  genpelvu  7646  addsrmo  7876  mulsrmo  7877  aptisr  7912  ltresr  7972  axcnre  8014  axpre-apti  8018  ltordlem  8575  apreap  8680  apreim  8696  aprcl  8739  aptap  8743  sup3exmid  9050  creur  9052  creui  9053  nn1m1nn  9074  nn1gt1  9090  elz  9394  nn0ind-raph  9510  nltpnft  9956  xnegeq  9969  xrpnfdc  9984  xrmnfdc  9985  xleaddadd  10029  flqeqceilz  10485  1tonninf  10608  iseqf1olemqval  10667  iseqf1olemqk  10674  seq3f1olemqsum  10680  exp3val  10708  wrd2ind  11199  shftfvalg  11204  shftfval  11207  summodc  11769  fsum3  11773  telfsumo  11852  mertenslemub  11920  mertenslemi1  11921  mertenslem2  11922  mertensabs  11923  prodmodc  11964  fprodseq  11969  fprodcl2lem  11991  ndvdssub  12316  gcdval  12355  bezoutlemnewy  12392  bezoutlema  12395  bezoutlemb  12396  lcmval  12460  coprmgcdb  12485  coprmdvds1  12488  divgcdcoprmex  12499  dvdsprime  12519  nprm  12520  dvdsprm  12534  coprm  12541  qnumval  12582  qdenval  12583  m1dvdsndvds  12646  reumodprminv  12651  pceu  12693  pcval  12694  pczpre  12695  pcdiv  12700  4sqlem2  12787  4sqlem4  12790  4sqlemafi  12793  4sqexercise1  12796  4sqexercise2  12797  4sqlemsdc  12798  4sqlem12  12800  4sq  12808  ennnfonelemj0  12847  ennnfonelemjn  12848  ennnfonelem0  12851  ennnfonelemp1  12852  ennnfonelemnn0  12868  ennnfonelemim  12870  unct  12888  gsum0g  13303  gsumval2  13304  ghmf1  13684  rrgeq0i  14101  domneq0  14109  lss1d  14220  lspsn  14253  ellspsn  14254  znf1o  14488  znidom  14494  znunit  14496  istopon  14560  toponsspwpwg  14569  epttop  14637  txuni2  14803  xmeteq0  14906  comet  15046  elply  15281  elply2  15282  mpodvdsmulf1o  15537  perfectlem2  15547  lgsval  15556  lgsfvalg  15557  lgsval2lem  15562  gausslemma2dlem0i  15609  2lgslem1b  15641  2lgslem3  15653  2sqlem2  15667  2sqlem8  15675  2sqlem9  15676  bj-charfunbi  15885  bj-nn0suc0  16024  bj-inf2vnlem1  16044  bj-inf2vnlem2  16045  bj-nn0sucALT  16052  subctctexmid  16078  pw1nct  16081  nnsf  16083  peano3nninf  16085  nninfall  16087  exmidsbthr  16103  trilpo  16123  trirec0  16124  redcwlpo  16135  redc0  16137  dceqnconst  16140