Theorem eqeq1 2236

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1393   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  eqeq1i  2237  eqeq1d  2238  eqeq2  2239  eqeq12  2242  eqtr  2247  eqsb1lem  2332  clelab  2355  neeq1  2413  pm13.18  2481  issetf  2808  sbhypf  2851  vtoclgft  2852  eqvincf  2929  pm13.183  2942  eueq  2975  mob  2986  euind  2991  reuind  3009  eqsbc1  3069  csbhypf  3164  uniiunlem  3314  snjust  3672  elsng  3682  elprg  3687  rabrsndc  3737  sneqrg  3843  preq12bg  3854  intab  3955  dfiin2g  4001  exmidsssnc  4291  exmid1stab  4296  opthg  4328  copsexg  4334  euotd  4345  elopab  4350  snnex  4543  uniuni  4546  eusv1  4547  reusv3  4555  ordtriexmid  4617  ontriexmidim  4618  onsucelsucexmidlem1  4624  onsucelsucexmid  4626  regexmidlemm  4628  regexmidlem1  4629  reg2exmidlema  4630  wetriext  4673  nn0suc  4700  nndceq0  4714  0elnn  4715  elxpi  4739  opbrop  4803  relop  4878  ideqg  4879  elrnmpt  4979  elrnmpt1  4981  elrnmptg  4982  restidsing  5067  cnveqb  5190  relcoi1  5266  funopg  5358  funcnvuni  5396  f0rn0  5528  fun11iun  5601  fvelrnb  5689  fvmptg  5718  fndmin  5750  eldmrexrn  5784  fmptco  5809  foco2  5889  elabrex  5893  elabrexg  5894  abrexco  5895  f1veqaeq  5905  f1oiso  5962  eusvobj2  5999  acexmidlema  6004  acexmidlemb  6005  acexmidlem2  6010  acexmidlemv  6011  oprabid  6045  mpofun  6118  elrnmpog  6129  elrnmpo  6130  ralrnmpo  6131  rexrnmpo  6132  ovi3  6154  ov6g  6155  ovelrn  6166  caovcang  6179  caovcan  6182  eloprabi  6356  dftpos4  6424  tfr1onlemaccex  6509  tfrcllemaccex  6522  elqsg  6749  qsel  6776  brecop  6789  eroveu  6790  erovlem  6791  th3qlem1  6801  th3q  6804  elixpsn  6899  ixpsnf1o  6900  2dom  6975  fundmen  6976  xpf1o  7025  nneneq  7038  tridc  7082  elssdc  7087  eqsndc  7088  prfidceq  7113  tpfidceq  7115  fisseneq  7119  fidcenumlemrks  7143  elfi  7161  supsnti  7195  isotilem  7196  updjudhcoinrg  7271  updjud  7272  omp1eom  7285  difinfsn  7290  ctmlemr  7298  ismkvnex  7345  omniwomnimkv  7357  nninfwlpoimlemginf  7366  nninfwlpoimlemdc  7367  nninfinfwlpolem  7368  exmidaclem  7413  exmidac  7414  onntri35  7445  exmidapne  7469  indpi  7552  nqtri3or  7606  enq0sym  7642  enq0ref  7643  enq0tr  7644  enq0breq  7646  addnq0mo  7657  mulnq0mo  7658  mulnnnq0  7660  genipv  7719  genpelvl  7722  genpelvu  7723  addsrmo  7953  mulsrmo  7954  aptisr  7989  ltresr  8049  axcnre  8091  axpre-apti  8095  ltordlem  8652  apreap  8757  apreim  8773  aprcl  8816  aptap  8820  sup3exmid  9127  creur  9129  creui  9130  nn1m1nn  9151  nn1gt1  9167  elz  9471  nn0ind-raph  9587  nltpnft  10039  xnegeq  10052  xrpnfdc  10067  xrmnfdc  10068  xleaddadd  10112  flqeqceilz  10570  1tonninf  10693  iseqf1olemqval  10752  iseqf1olemqk  10759  seq3f1olemqsum  10765  exp3val  10793  wrd2ind  11294  shftfvalg  11369  shftfval  11372  summodc  11934  fsum3  11938  telfsumo  12017  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodmodc  12129  fprodseq  12134  fprodcl2lem  12156  ndvdssub  12481  gcdval  12520  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  lcmval  12625  coprmgcdb  12650  coprmdvds1  12653  divgcdcoprmex  12664  dvdsprime  12684  nprm  12685  dvdsprm  12699  coprm  12706  qnumval  12747  qdenval  12748  m1dvdsndvds  12811  reumodprminv  12816  pceu  12858  pcval  12859  pczpre  12860  pcdiv  12865  4sqlem2  12952  4sqlem4  12955  4sqlemafi  12958  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  4sqlem12  12965  4sq  12973  ennnfonelemj0  13012  ennnfonelemjn  13013  ennnfonelem0  13016  ennnfonelemp1  13017  ennnfonelemnn0  13033  ennnfonelemim  13035  unct  13053  gsum0g  13469  gsumval2  13470  ghmf1  13850  rrgeq0i  14268  domneq0  14276  lss1d  14387  lspsn  14420  ellspsn  14421  znf1o  14655  znidom  14661  znunit  14663  istopon  14727  toponsspwpwg  14736  epttop  14804  txuni2  14970  xmeteq0  15073  comet  15213  elply  15448  elply2  15449  mpodvdsmulf1o  15704  perfectlem2  15714  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  gausslemma2dlem0i  15776  2lgslem1b  15808  2lgslem3  15820  2sqlem2  15834  2sqlem8  15842  2sqlem9  15843  upgredg2vtx  15987  uspgredg2v  16060  ushgredgedgloop  16067  vtxduspgrfvedgfi  16107  1loopgrvd2fi  16111  wlkeq  16151  bj-charfunbi  16342  bj-nn0suc0  16481  bj-inf2vnlem1  16501  bj-inf2vnlem2  16502  bj-nn0sucALT  16509  subctctexmid  16537  pw1nct  16540  nnsf  16543  peano3nninf  16545  nninfall  16547  exmidsbthr  16563  trilpo  16583  trirec0  16584  redcwlpo  16595  redc0  16597  dceqnconst  16600