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  2807  sbhypf  2850  vtoclgft  2851  eqvincf  2928  pm13.183  2941  eueq  2974  mob  2985  euind  2990  reuind  3008  eqsbc1  3068  csbhypf  3163  uniiunlem  3313  snjust  3671  elsng  3681  elprg  3686  rabrsndc  3734  sneqrg  3840  preq12bg  3851  intab  3952  dfiin2g  3998  exmidsssnc  4287  exmid1stab  4292  opthg  4324  copsexg  4330  euotd  4341  elopab  4346  snnex  4539  uniuni  4542  eusv1  4543  reusv3  4551  ordtriexmid  4613  ontriexmidim  4614  onsucelsucexmidlem1  4620  onsucelsucexmid  4622  regexmidlemm  4624  regexmidlem1  4625  reg2exmidlema  4626  wetriext  4669  nn0suc  4696  nndceq0  4710  0elnn  4711  elxpi  4735  opbrop  4798  relop  4872  ideqg  4873  elrnmpt  4973  elrnmpt1  4975  elrnmptg  4976  restidsing  5061  cnveqb  5184  relcoi1  5260  funopg  5352  funcnvuni  5390  f0rn0  5522  fun11iun  5595  fvelrnb  5683  fvmptg  5712  fndmin  5744  eldmrexrn  5778  fmptco  5803  foco2  5883  elabrex  5887  elabrexg  5888  abrexco  5889  f1veqaeq  5899  f1oiso  5956  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  acexmidlemv  6005  oprabid  6039  mpofun  6112  elrnmpog  6123  elrnmpo  6124  ralrnmpo  6125  rexrnmpo  6126  ovi3  6148  ov6g  6149  ovelrn  6160  caovcang  6173  caovcan  6176  eloprabi  6348  dftpos4  6415  tfr1onlemaccex  6500  tfrcllemaccex  6513  elqsg  6740  qsel  6767  brecop  6780  eroveu  6781  erovlem  6782  th3qlem1  6792  th3q  6795  elixpsn  6890  ixpsnf1o  6891  2dom  6966  fundmen  6967  xpf1o  7013  nneneq  7026  tridc  7070  elssdc  7075  eqsndc  7076  prfidceq  7101  tpfidceq  7103  fisseneq  7107  fidcenumlemrks  7131  elfi  7149  supsnti  7183  isotilem  7184  updjudhcoinrg  7259  updjud  7260  omp1eom  7273  difinfsn  7278  ctmlemr  7286  ismkvnex  7333  omniwomnimkv  7345  nninfwlpoimlemginf  7354  nninfwlpoimlemdc  7355  nninfinfwlpolem  7356  exmidaclem  7401  exmidac  7402  onntri35  7433  exmidapne  7457  indpi  7540  nqtri3or  7594  enq0sym  7630  enq0ref  7631  enq0tr  7632  enq0breq  7634  addnq0mo  7645  mulnq0mo  7646  mulnnnq0  7648  genipv  7707  genpelvl  7710  genpelvu  7711  addsrmo  7941  mulsrmo  7942  aptisr  7977  ltresr  8037  axcnre  8079  axpre-apti  8083  ltordlem  8640  apreap  8745  apreim  8761  aprcl  8804  aptap  8808  sup3exmid  9115  creur  9117  creui  9118  nn1m1nn  9139  nn1gt1  9155  elz  9459  nn0ind-raph  9575  nltpnft  10022  xnegeq  10035  xrpnfdc  10050  xrmnfdc  10051  xleaddadd  10095  flqeqceilz  10552  1tonninf  10675  iseqf1olemqval  10734  iseqf1olemqk  10741  seq3f1olemqsum  10747  exp3val  10775  wrd2ind  11270  shftfvalg  11344  shftfval  11347  summodc  11909  fsum3  11913  telfsumo  11992  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodmodc  12104  fprodseq  12109  fprodcl2lem  12131  ndvdssub  12456  gcdval  12495  bezoutlemnewy  12532  bezoutlema  12535  bezoutlemb  12536  lcmval  12600  coprmgcdb  12625  coprmdvds1  12628  divgcdcoprmex  12639  dvdsprime  12659  nprm  12660  dvdsprm  12674  coprm  12681  qnumval  12722  qdenval  12723  m1dvdsndvds  12786  reumodprminv  12791  pceu  12833  pcval  12834  pczpre  12835  pcdiv  12840  4sqlem2  12927  4sqlem4  12930  4sqlemafi  12933  4sqexercise1  12936  4sqexercise2  12937  4sqlemsdc  12938  4sqlem12  12940  4sq  12948  ennnfonelemj0  12987  ennnfonelemjn  12988  ennnfonelem0  12991  ennnfonelemp1  12992  ennnfonelemnn0  13008  ennnfonelemim  13010  unct  13028  gsum0g  13444  gsumval2  13445  ghmf1  13825  rrgeq0i  14243  domneq0  14251  lss1d  14362  lspsn  14395  ellspsn  14396  znf1o  14630  znidom  14636  znunit  14638  istopon  14702  toponsspwpwg  14711  epttop  14779  txuni2  14945  xmeteq0  15048  comet  15188  elply  15423  elply2  15424  mpodvdsmulf1o  15679  perfectlem2  15689  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  gausslemma2dlem0i  15751  2lgslem1b  15783  2lgslem3  15795  2sqlem2  15809  2sqlem8  15817  2sqlem9  15818  upgredg2vtx  15961  uspgredg2v  16034  ushgredgedgloop  16041  wlkeq  16095  bj-charfunbi  16229  bj-nn0suc0  16368  bj-inf2vnlem1  16388  bj-inf2vnlem2  16389  bj-nn0sucALT  16396  subctctexmid  16425  pw1nct  16428  nnsf  16431  peano3nninf  16433  nninfall  16435  exmidsbthr  16451  trilpo  16471  trirec0  16472  redcwlpo  16483  redc0  16485  dceqnconst  16488