Theorem eqeq1 2245

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 2232	. . . . . 6 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2	1	biimpi 120	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
3	2	19.21bi 1611	. . . 4 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
4	3	bibi1d 233	. . 3 ⊢ (𝐴 = 𝐵 → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
5	4	albidv 1877	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶)))
6		dfcleq 2232	. 2 ⊢ (𝐴 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
7		dfcleq 2232	. 2 ⊢ (𝐵 = 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 ↔ 𝑥 ∈ 𝐶))
8	5, 6, 7	3bitr4g 223	1 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1400   = wceq 1402   ∈ wcel 2209

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  eqeq1i  2246  eqeq1d  2247  eqeq2  2248  eqeq12  2251  eqtr  2256  eqsb1lem  2341  clelab  2366  neeq1  2433  pm13.18  2501  issetf  2829  sbhypf  2872  vtoclgft  2873  eqvincf  2951  pm13.183  2964  eueq  2997  mob  3008  euind  3013  reuind  3031  eqsbc1  3091  csbhypf  3186  uniiunlem  3338  snjust  3710  elsng  3720  elprg  3725  rabrsndc  3775  sneqrg  3882  preq12bg  3893  intab  3994  dfiin2g  4040  exmidsssnc  4335  exmid1stab  4340  opthg  4373  copsexg  4379  euotd  4390  elopab  4395  snnex  4589  uniuni  4592  eusv1  4593  reusv3  4601  ordtriexmid  4663  ontriexmidim  4664  onsucelsucexmidlem1  4670  onsucelsucexmid  4672  regexmidlemm  4674  regexmidlem1  4675  reg2exmidlema  4676  wetriext  4719  nn0suc  4746  nndceq0  4760  0elnn  4761  elxpi  4785  opbrop  4849  relop  4925  ideqg  4926  elrnmpt  5026  elrnmpt1  5028  elrnmptg  5029  restidsing  5114  cnveqb  5238  relcoi1  5314  funopg  5406  funcnvuni  5445  f0rn0  5582  fun11iun  5655  fvelrnb  5744  fvmptg  5775  fndmin  5807  eldmrexrn  5840  fmptco  5865  foco2  5949  elabrex  5953  elabrexg  5954  abrexco  5955  f1veqaeq  5965  f1oiso  6022  eusvobj2  6061  acexmidlema  6066  acexmidlemb  6067  acexmidlem2  6072  acexmidlemv  6073  oprabid  6107  mpofun  6180  elrnmpog  6191  elrnmpo  6192  ralrnmpo  6193  rexrnmpo  6194  ovi3  6216  ov6g  6217  ovelrn  6228  caovcang  6241  caovcan  6244  elabreximd  6346  eloprabi  6422  funsssuppss  6488  suppssrst  6491  suppssrgst  6492  dftpos4  6524  tfr1onlemaccex  6609  tfrcllemaccex  6622  elqsg  6849  qsel  6876  brecop  6889  eroveu  6890  erovlem  6891  th3qlem1  6901  th3q  6904  elixpsn  7007  ixpsnf1o  7008  2dom  7083  fundmen  7084  xpf1o  7134  nneneq  7148  tridc  7194  elssdc  7199  eqsndc  7200  prfidceq  7225  tpfidceq  7227  fisseneq  7232  fidcenumlemrks  7260  elfi  7295  supsnti  7335  isotilem  7336  updjudhcoinrg  7411  updjud  7412  omp1eom  7425  difinfsn  7430  ctmlemr  7438  ismkvnex  7485  omniwomnimkv  7497  nninfwlpoimlemginf  7506  nninfwlpoimlemdc  7507  nninfinfwlpolem  7508  exmidaclem  7554  exmidac  7555  onntri35  7586  exmidapne  7616  indpi  7699  nqtri3or  7753  enq0sym  7789  enq0ref  7790  enq0tr  7791  enq0breq  7793  addnq0mo  7804  mulnq0mo  7805  mulnnnq0  7807  genipv  7866  genpelvl  7869  genpelvu  7870  addsrmo  8100  mulsrmo  8101  aptisr  8136  ltresr  8196  axcnre  8238  axpre-apti  8242  ltordlem  8800  apreap  8905  apreim  8921  aprcl  8964  aptap  8968  sup3exmid  9277  creur  9279  creui  9280  nn1m1nn  9301  nn1gt1  9317  elz  9625  nn0ind-raph  9742  nltpnft  10195  xnegeq  10208  xrpnfdc  10223  xrmnfdc  10224  xleaddadd  10268  flqeqceilz  10733  1tonninf  10856  iseqf1olemqval  10915  iseqf1olemqk  10922  seq3f1olemqsum  10928  exp3val  10956  wrd2ind  11473  shftfvalg  11561  shftfval  11564  summodc  12128  fsum3  12132  telfsumo  12211  mertenslemub  12279  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  prodmodc  12323  fprodseq  12328  fprodcl2lem  12350  ndvdssub  12675  gcdval  12714  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  lcmval  12819  coprmgcdb  12844  coprmdvds1  12847  divgcdcoprmex  12858  dvdsprime  12878  nprm  12879  dvdsprm  12893  coprm  12900  qnumval  12941  qdenval  12942  m1dvdsndvds  13005  reumodprminv  13010  pceu  13052  pcval  13053  pczpre  13054  pcdiv  13059  4sqlem2  13146  4sqlem4  13149  4sqlemafi  13152  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  4sqlem12  13159  4sq  13167  ballotfilem2  13206  ennnfonelemj0  13270  ennnfonelemjn  13271  ennnfonelem0  13274  ennnfonelemp1  13275  ennnfonelemnn0  13291  ennnfonelemim  13293  unct  13311  gzsum0  13690  gzsumval2  13691  ghmf1  14053  gsumvalfi  14129  rrgeq0i  14545  domneq0  14554  lss1d  14692  lspsn  14725  ellspsn  14726  znf1o  14958  znidom  14964  znunit  14966  istopon  15037  toponsspwpwg  15046  epttop  15114  txuni2  15280  xmeteq0  15383  comet  15523  elply  15758  elply2  15759  mpodvdsmulf1o  16018  perfectlem2  16028  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  gausslemma2dlem0i  16090  2lgslem1b  16122  2lgslem3  16134  2sqlem2  16148  2sqlem8  16156  2sqlem9  16157  upgredg2vtx  16303  uspgredg2v  16376  ushgredgedgloop  16383  vtxduspgrfvedgfi  16456  1loopgrvd2fi  16460  wlkeq  16509  depindlem1  16661  bj-charfunbi  16751  bj-nn0suc0  16890  bj-inf2vnlem1  16910  bj-inf2vnlem2  16911  bj-nn0sucALT  16918  subctctexmid  16944  pw1nct  16947  exmidnotnotr  16949  exmidcon  16950  exmidpeirce  16951  nnsf  16953  peano3nninf  16955  nninfall  16957  exmidsbthr  16973  trilpo  16997  trirec0  16998  redcwlpo  17010  redc0  17012  dceqnconst  17015