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  3839  preq12bg  3850  intab  3951  dfiin2g  3997  exmidsssnc  4286  exmid1stab  4291  opthg  4323  copsexg  4329  euotd  4340  elopab  4345  snnex  4538  uniuni  4541  eusv1  4542  reusv3  4550  ordtriexmid  4612  ontriexmidim  4613  onsucelsucexmidlem1  4619  onsucelsucexmid  4621  regexmidlemm  4623  regexmidlem1  4624  reg2exmidlema  4625  wetriext  4668  nn0suc  4695  nndceq0  4709  0elnn  4710  elxpi  4734  opbrop  4797  relop  4871  ideqg  4872  elrnmpt  4972  elrnmpt1  4974  elrnmptg  4975  restidsing  5060  cnveqb  5183  relcoi1  5259  funopg  5351  funcnvuni  5389  f0rn0  5519  fun11iun  5592  fvelrnb  5680  fvmptg  5709  fndmin  5741  eldmrexrn  5775  fmptco  5800  foco2  5876  elabrex  5880  elabrexg  5881  abrexco  5882  f1veqaeq  5892  f1oiso  5949  eusvobj2  5986  acexmidlema  5991  acexmidlemb  5992  acexmidlem2  5997  acexmidlemv  5998  oprabid  6032  mpofun  6105  elrnmpog  6116  elrnmpo  6117  ralrnmpo  6118  rexrnmpo  6119  ovi3  6141  ov6g  6142  ovelrn  6153  caovcang  6166  caovcan  6169  eloprabi  6340  dftpos4  6407  tfr1onlemaccex  6492  tfrcllemaccex  6505  elqsg  6730  qsel  6757  brecop  6770  eroveu  6771  erovlem  6772  th3qlem1  6782  th3q  6785  elixpsn  6880  ixpsnf1o  6881  2dom  6956  fundmen  6957  xpf1o  7001  nneneq  7014  tridc  7057  prfidceq  7086  tpfidceq  7088  fisseneq  7092  fidcenumlemrks  7116  elfi  7134  supsnti  7168  isotilem  7169  updjudhcoinrg  7244  updjud  7245  omp1eom  7258  difinfsn  7263  ctmlemr  7271  ismkvnex  7318  omniwomnimkv  7330  nninfwlpoimlemginf  7339  nninfwlpoimlemdc  7340  nninfinfwlpolem  7341  exmidaclem  7386  exmidac  7387  onntri35  7418  exmidapne  7442  indpi  7525  nqtri3or  7579  enq0sym  7615  enq0ref  7616  enq0tr  7617  enq0breq  7619  addnq0mo  7630  mulnq0mo  7631  mulnnnq0  7633  genipv  7692  genpelvl  7695  genpelvu  7696  addsrmo  7926  mulsrmo  7927  aptisr  7962  ltresr  8022  axcnre  8064  axpre-apti  8068  ltordlem  8625  apreap  8730  apreim  8746  aprcl  8789  aptap  8793  sup3exmid  9100  creur  9102  creui  9103  nn1m1nn  9124  nn1gt1  9140  elz  9444  nn0ind-raph  9560  nltpnft  10006  xnegeq  10019  xrpnfdc  10034  xrmnfdc  10035  xleaddadd  10079  flqeqceilz  10535  1tonninf  10658  iseqf1olemqval  10717  iseqf1olemqk  10724  seq3f1olemqsum  10730  exp3val  10758  wrd2ind  11250  shftfvalg  11324  shftfval  11327  summodc  11889  fsum3  11893  telfsumo  11972  mertenslemub  12040  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  prodmodc  12084  fprodseq  12089  fprodcl2lem  12111  ndvdssub  12436  gcdval  12475  bezoutlemnewy  12512  bezoutlema  12515  bezoutlemb  12516  lcmval  12580  coprmgcdb  12605  coprmdvds1  12608  divgcdcoprmex  12619  dvdsprime  12639  nprm  12640  dvdsprm  12654  coprm  12661  qnumval  12702  qdenval  12703  m1dvdsndvds  12766  reumodprminv  12771  pceu  12813  pcval  12814  pczpre  12815  pcdiv  12820  4sqlem2  12907  4sqlem4  12910  4sqlemafi  12913  4sqexercise1  12916  4sqexercise2  12917  4sqlemsdc  12918  4sqlem12  12920  4sq  12928  ennnfonelemj0  12967  ennnfonelemjn  12968  ennnfonelem0  12971  ennnfonelemp1  12972  ennnfonelemnn0  12988  ennnfonelemim  12990  unct  13008  gsum0g  13424  gsumval2  13425  ghmf1  13805  rrgeq0i  14222  domneq0  14230  lss1d  14341  lspsn  14374  ellspsn  14375  znf1o  14609  znidom  14615  znunit  14617  istopon  14681  toponsspwpwg  14690  epttop  14758  txuni2  14924  xmeteq0  15027  comet  15167  elply  15402  elply2  15403  mpodvdsmulf1o  15658  perfectlem2  15668  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  gausslemma2dlem0i  15730  2lgslem1b  15762  2lgslem3  15774  2sqlem2  15788  2sqlem8  15796  2sqlem9  15797  upgredg2vtx  15940  uspgredg2v  16013  ushgredgedgloop  16020  bj-charfunbi  16132  bj-nn0suc0  16271  bj-inf2vnlem1  16291  bj-inf2vnlem2  16292  bj-nn0sucALT  16299  subctctexmid  16325  pw1nct  16328  nnsf  16330  peano3nninf  16332  nninfall  16334  exmidsbthr  16350  trilpo  16370  trirec0  16371  redcwlpo  16382  redc0  16384  dceqnconst  16387