Theorem eqeq1 2046

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 2034	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 113	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1450	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 222	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1705	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2034	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2034	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 212	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1241   = wceq 1243   ∈ wcel 1393

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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022

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

This theorem is referenced by:  eqeq1i  2047  eqeq1d  2048  eqeq2  2049  eqeq12  2052  eqtr  2057  eqsb3lem  2140  clelab  2162  neeq1  2218  pm13.18  2286  issetf  2562  sbhypf  2603  vtoclgft  2604  eqvincf  2669  pm13.183  2681  eueq  2712  mob  2723  euind  2728  reuind  2744  eqsbc3  2802  csbhypf  2885  uniiunlem  3028  snjust  3380  elsng  3390  elprg  3395  rabrsndc  3438  sneqrg  3533  preq12bg  3544  intab  3644  dfiin2g  3690  opthg  3975  copsexg  3981  euotd  3991  elopab  3995  snnex  4181  uniuni  4183  eusv1  4184  reusv3  4192  ordtriexmid  4247  onsucelsucexmidlem1  4253  onsucelsucexmid  4255  regexmidlemm  4257  regexmidlem1  4258  reg2exmidlema  4259  wetriext  4301  nn0suc  4327  nndceq0  4339  0elnn  4340  elxpi  4361  opbrop  4419  relop  4486  ideqg  4487  elrnmpt  4583  elrnmpt1  4585  elrnmptg  4586  cnveqb  4776  relcoi1  4849  funopg  4934  funcnvuni  4968  fun11iun  5147  fvelrnb  5221  fvmptg  5248  fndmin  5274  eldmrexrn  5308  foelrn  5317  foco2  5318  fmptco  5330  elabrex  5397  abrexco  5398  f1veqaeq  5408  f1oiso  5465  eusvobj2  5498  acexmidlema  5503  acexmidlemb  5504  acexmidlem2  5509  acexmidlemv  5510  oprabid  5537  mpt2fun  5603  elrnmpt2g  5613  elrnmpt2  5614  ralrnmpt2  5615  rexrnmpt2  5616  ovi3  5637  ov6g  5638  ovelrn  5649  caovcang  5662  caovcan  5665  eloprabi  5822  dftpos4  5878  elqsg  6156  qsel  6183  brecop  6196  eroveu  6197  erovlem  6198  th3qlem1  6208  th3q  6211  2dom  6285  fundmen  6286  nneneq  6320  indpi  6440  nqtri3or  6494  enq0sym  6530  enq0ref  6531  enq0tr  6532  enq0breq  6534  addnq0mo  6545  mulnq0mo  6546  mulnnnq0  6548  genipv  6607  genpelvl  6610  genpelvu  6611  addsrmo  6828  mulsrmo  6829  aptisr  6863  ltresr  6915  axcnre  6955  axpre-apti  6959  apreap  7578  apreim  7594  creur  7911  creui  7912  nn1m1nn  7932  nn1gt1  7947  elz  8247  nn0ind-raph  8355  nltpnft  8730  xnegeq  8740  flqeqceilz  9160  expival  9257  shftfvalg  9419  shftfval  9422  bj-nn0suc0  10075  bj-inf2vnlem1  10095  bj-inf2vnlem2  10096  bj-nn0sucALT  10103