Theorem eqeq1 2022

Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
eqeq1	⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))

Proof of Theorem eqeq1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfcleq 2010	. . . . . 6 ⊢ (A = B ↔ ∀x(x ∈ A ↔ x ∈ B))
2	1	biimpi 113	. . . . 5 ⊢ (A = B → ∀x(x ∈ A ↔ x ∈ B))
3	2	19.21bi 1426	. . . 4 ⊢ (A = B → (x ∈ A ↔ x ∈ B))
4	3	bibi1d 222	. . 3 ⊢ (A = B → ((x ∈ A ↔ x ∈ 𝐶) ↔ (x ∈ B ↔ x ∈ 𝐶)))
5	4	albidv 1681	. 2 ⊢ (A = B → (∀x(x ∈ A ↔ x ∈ 𝐶) ↔ ∀x(x ∈ B ↔ x ∈ 𝐶)))
6		dfcleq 2010	. 2 ⊢ (A = 𝐶 ↔ ∀x(x ∈ A ↔ x ∈ 𝐶))
7		dfcleq 2010	. 2 ⊢ (B = 𝐶 ↔ ∀x(x ∈ B ↔ x ∈ 𝐶))
8	5, 6, 7	3bitr4g 212	1 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶))

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1224   = wceq 1226   ∈ wcel 1369

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-gen 1314  ax-4 1376  ax-17 1395  ax-ext 1998

This theorem depends on definitions:  df-bi 110  df-cleq 2009

This theorem is referenced by:  eqeq1i  2023  eqeq1d  2024  eqeq2  2025  eqeq12  2028  eqtr  2033  eqsb3lem  2116  clelab  2138  neeq1  2191  pm13.18  2258  issetf  2534  sbhypf  2574  vtoclgft  2575  eqvincf  2640  pm13.183  2652  eueq  2683  mob  2694  euind  2699  reuind  2715  eqsbc3  2773  csbhypf  2856  uniiunlem  2999  snjust  3347  elprg  3359  elsncg  3364  rabrsndc  3404  sneqrg  3499  preq12bg  3510  intab  3610  dfiin2g  3656  opthg  3941  copsexg  3947  euotd  3957  elopab  3961  snnex  4122  uniuni  4124  eusv1  4125  reusv3  4133  ordtriexmid  4185  onsucelsucexmidlem1  4188  onsucelsucexmid  4190  regexmidlemm  4192  regexmidlem1  4193  nn0suc  4245  nndceq0  4257  0elnn  4258  elxpi  4279  opbrop  4337  relop  4404  ideqg  4405  elrnmpt  4501  elrnmpt1  4503  elrnmptg  4504  cnveqb  4694  relcoi1  4767  funopg  4851  funcnvuni  4885  fun11iun  5063  fvelrnb  5137  fvmptg  5164  fndmin  5190  eldmrexrn  5224  foelrn  5233  foco2  5234  fmptco  5246  elabrex  5313  abrexco  5314  f1veqaeq  5324  f1oiso  5381  eusvobj2  5413  acexmidlema  5418  acexmidlemb  5419  acexmidlem2  5424  acexmidlemv  5425  oprabid  5452  mpt2fun  5517  elrnmpt2g  5527  elrnmpt2  5528  ralrnmpt2  5529  rexrnmpt2  5530  ovi3  5551  ov6g  5552  ovelrn  5563  caovcang  5576  caovcan  5579  eloprabi  5736  dftpos4  5791  elqsg  6058  qsel  6085  brecop  6098  eroveu  6099  erovlem  6100  th3qlem1  6110  th3q  6113  nqtri3or  6244  enq0sym  6276  enq0ref  6277  enq0tr  6278  enq0breq  6280  addnq0mo  6291  mulnq0mo  6292  mulnnnq0  6294  genipv  6352  genpelvl  6355  genpelvu  6356  addsrmo  6484  mulsrmo  6485  aptisr  6518  ltresr  6548  axcnre  6573  axpre-apti  6577  apreap  7177  apreim  7193  creur  7497  creui  7498  nn1m1nn  7518  nn1gt1  7533  elz  7824  nn0ind-raph  7923  nltpnft  8209  xnegeq  8219  bj-nn0suc0  8526  bj-inf2vnlem1  8542  bj-inf2vnlem2  8543  bj-nn0sucALT  8550