Theorem eqeq1 2106

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 2094	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 119	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1505	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 232	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1763	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2094	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2094	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 222	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1297   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093

This theorem is referenced by:  eqeq1i  2107  eqeq1d  2108  eqeq2  2109  eqeq12  2112  eqtr  2117  eqsb3lem  2202  clelab  2224  neeq1  2280  pm13.18  2348  issetf  2648  sbhypf  2690  vtoclgft  2691  eqvincf  2764  pm13.183  2776  eueq  2808  mob  2819  euind  2824  reuind  2842  eqsbc3  2900  csbhypf  2988  uniiunlem  3132  snjust  3479  elsng  3489  elprg  3494  rabrsndc  3538  sneqrg  3636  preq12bg  3647  intab  3747  dfiin2g  3793  exmidsssnc  4064  opthg  4098  copsexg  4104  euotd  4114  elopab  4118  snnex  4307  uniuni  4310  eusv1  4311  reusv3  4319  ordtriexmid  4375  onsucelsucexmidlem1  4381  onsucelsucexmid  4383  regexmidlemm  4385  regexmidlem1  4386  reg2exmidlema  4387  wetriext  4429  nn0suc  4456  nndceq0  4469  0elnn  4470  elxpi  4493  opbrop  4556  relop  4627  ideqg  4628  elrnmpt  4726  elrnmpt1  4728  elrnmptg  4729  cnveqb  4930  relcoi1  5006  funopg  5093  funcnvuni  5128  f0rn0  5253  fun11iun  5322  fvelrnb  5401  fvmptg  5429  fndmin  5459  eldmrexrn  5493  fmptco  5518  foco2  5587  elabrex  5591  abrexco  5592  f1veqaeq  5602  f1oiso  5659  eusvobj2  5692  acexmidlema  5697  acexmidlemb  5698  acexmidlem2  5703  acexmidlemv  5704  oprabid  5735  mpofun  5805  elrnmpog  5815  elrnmpo  5816  ralrnmpo  5817  rexrnmpo  5818  ovi3  5839  ov6g  5840  ovelrn  5851  caovcang  5864  caovcan  5867  eloprabi  6024  dftpos4  6090  tfr1onlemaccex  6175  tfrcllemaccex  6188  elqsg  6409  qsel  6436  brecop  6449  eroveu  6450  erovlem  6451  th3qlem1  6461  th3q  6464  elixpsn  6559  ixpsnf1o  6560  2dom  6629  fundmen  6630  xpf1o  6667  nneneq  6680  tridc  6722  fisseneq  6749  fidcenumlemrks  6769  supsnti  6807  isotilem  6808  updjudhcoinrg  6881  updjud  6882  omp1eom  6895  difinfsn  6900  ctmlemr  6908  indpi  7051  nqtri3or  7105  enq0sym  7141  enq0ref  7142  enq0tr  7143  enq0breq  7145  addnq0mo  7156  mulnq0mo  7157  mulnnnq0  7159  genipv  7218  genpelvl  7221  genpelvu  7222  addsrmo  7439  mulsrmo  7440  aptisr  7474  ltresr  7526  axcnre  7566  axpre-apti  7570  ltordlem  8111  apreap  8215  apreim  8231  sup3exmid  8573  creur  8575  creui  8576  nn1m1nn  8596  nn1gt1  8612  elz  8908  nn0ind-raph  9020  nltpnft  9438  xnegeq  9451  xrpnfdc  9466  xrmnfdc  9467  xleaddadd  9511  flqeqceilz  9932  1tonninf  10054  iseqf1olemqval  10101  iseqf1olemqk  10108  seq3f1olemqsum  10114  exp3val  10136  shftfvalg  10431  shftfval  10434  summodc  10991  fsum3  10995  telfsumo  11074  mertenslemub  11142  mertenslemi1  11143  mertenslem2  11144  mertensabs  11145  ndvdssub  11422  gcdval  11443  bezoutlemnewy  11477  bezoutlema  11480  bezoutlemb  11481  lcmval  11537  coprmgcdb  11562  coprmdvds1  11565  divgcdcoprmex  11576  dvdsprime  11596  nprm  11597  dvdsprm  11610  coprm  11615  qnumval  11655  qdenval  11656  ennnfonelemj0  11706  ennnfonelemjn  11707  ennnfonelem0  11710  ennnfonelemp1  11711  ennnfonelemnn0  11727  ennnfonelemim  11729  istopon  11962  toponsspwpwg  11971  epttop  12041  txuni2  12206  xmeteq0  12287  comet  12427  bj-nn0suc0  12733  bj-inf2vnlem1  12753  bj-inf2vnlem2  12754  bj-nn0sucALT  12761  nnsf  12783  peano3nninf  12785  nninfall  12788  exmidsbthr  12802  trilpo  12820