ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeq1 GIF version

Theorem eqeq1 2184
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.
StepHypRef Expression
1 dfcleq 2171 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 120 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1558 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43bibi1d 233 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
54albidv 1824 . 2 (𝐴 = 𝐵 → (∀𝑥(𝑥𝐴𝑥𝐶) ↔ ∀𝑥(𝑥𝐵𝑥𝐶)))
6 dfcleq 2171 . 2 (𝐴 = 𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
7 dfcleq 2171 . 2 (𝐵 = 𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
85, 6, 73bitr4g 223 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wal 1351   = wceq 1353  wcel 2148
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqeq1i  2185  eqeq1d  2186  eqeq2  2187  eqeq12  2190  eqtr  2195  eqsb1lem  2280  clelab  2303  neeq1  2360  pm13.18  2428  issetf  2744  sbhypf  2786  vtoclgft  2787  eqvincf  2862  pm13.183  2875  eueq  2908  mob  2919  euind  2924  reuind  2942  eqsbc1  3002  csbhypf  3095  uniiunlem  3244  snjust  3596  elsng  3606  elprg  3611  rabrsndc  3659  sneqrg  3760  preq12bg  3771  intab  3871  dfiin2g  3917  exmidsssnc  4200  exmid1stab  4205  opthg  4235  copsexg  4241  euotd  4251  elopab  4255  snnex  4445  uniuni  4448  eusv1  4449  reusv3  4457  ordtriexmid  4517  ontriexmidim  4518  onsucelsucexmidlem1  4524  onsucelsucexmid  4526  regexmidlemm  4528  regexmidlem1  4529  reg2exmidlema  4530  wetriext  4573  nn0suc  4600  nndceq0  4614  0elnn  4615  elxpi  4639  opbrop  4702  relop  4773  ideqg  4774  elrnmpt  4872  elrnmpt1  4874  elrnmptg  4875  restidsing  4959  cnveqb  5080  relcoi1  5156  funopg  5246  funcnvuni  5281  f0rn0  5406  fun11iun  5478  fvelrnb  5559  fvmptg  5588  fndmin  5619  eldmrexrn  5653  fmptco  5678  foco2  5749  elabrex  5753  abrexco  5754  f1veqaeq  5764  f1oiso  5821  eusvobj2  5855  acexmidlema  5860  acexmidlemb  5861  acexmidlem2  5866  acexmidlemv  5867  oprabid  5901  mpofun  5971  elrnmpog  5981  elrnmpo  5982  ralrnmpo  5983  rexrnmpo  5984  ovi3  6005  ov6g  6006  ovelrn  6017  caovcang  6030  caovcan  6033  eloprabi  6191  dftpos4  6258  tfr1onlemaccex  6343  tfrcllemaccex  6356  elqsg  6579  qsel  6606  brecop  6619  eroveu  6620  erovlem  6621  th3qlem1  6631  th3q  6634  elixpsn  6729  ixpsnf1o  6730  2dom  6799  fundmen  6800  xpf1o  6838  nneneq  6851  tridc  6893  fisseneq  6925  fidcenumlemrks  6946  elfi  6964  supsnti  6998  isotilem  6999  updjudhcoinrg  7074  updjud  7075  omp1eom  7088  difinfsn  7093  ctmlemr  7101  ismkvnex  7147  omniwomnimkv  7159  nninfwlpoimlemginf  7168  nninfwlpoimlemdc  7169  exmidaclem  7201  exmidac  7202  onntri35  7230  exmidapne  7250  indpi  7332  nqtri3or  7386  enq0sym  7422  enq0ref  7423  enq0tr  7424  enq0breq  7426  addnq0mo  7437  mulnq0mo  7438  mulnnnq0  7440  genipv  7499  genpelvl  7502  genpelvu  7503  addsrmo  7733  mulsrmo  7734  aptisr  7769  ltresr  7829  axcnre  7871  axpre-apti  7875  ltordlem  8429  apreap  8534  apreim  8550  aprcl  8593  sup3exmid  8903  creur  8905  creui  8906  nn1m1nn  8926  nn1gt1  8942  elz  9244  nn0ind-raph  9359  nltpnft  9801  xnegeq  9814  xrpnfdc  9829  xrmnfdc  9830  xleaddadd  9874  flqeqceilz  10304  1tonninf  10426  iseqf1olemqval  10473  iseqf1olemqk  10480  seq3f1olemqsum  10486  exp3val  10508  shftfvalg  10811  shftfval  10814  summodc  11375  fsum3  11379  telfsumo  11458  mertenslemub  11526  mertenslemi1  11527  mertenslem2  11528  mertensabs  11529  prodmodc  11570  fprodseq  11575  fprodcl2lem  11597  ndvdssub  11918  gcdval  11943  bezoutlemnewy  11980  bezoutlema  11983  bezoutlemb  11984  lcmval  12046  coprmgcdb  12071  coprmdvds1  12074  divgcdcoprmex  12085  dvdsprime  12105  nprm  12106  dvdsprm  12120  coprm  12127  qnumval  12168  qdenval  12169  m1dvdsndvds  12231  reumodprminv  12236  pceu  12278  pcval  12279  pczpre  12280  pcdiv  12285  4sqlem2  12370  4sqlem4  12373  ennnfonelemj0  12385  ennnfonelemjn  12386  ennnfonelem0  12389  ennnfonelemp1  12390  ennnfonelemnn0  12406  ennnfonelemim  12408  unct  12426  istopon  13178  toponsspwpwg  13187  epttop  13257  txuni2  13423  xmeteq0  13526  comet  13666  lgsval  14072  lgsfvalg  14073  lgsval2lem  14078  2sqlem2  14118  2sqlem8  14126  2sqlem9  14127  bj-charfunbi  14219  bj-nn0suc0  14358  bj-inf2vnlem1  14378  bj-inf2vnlem2  14379  bj-nn0sucALT  14386  subctctexmid  14406  pw1nct  14408  nnsf  14410  peano3nninf  14412  nninfall  14414  exmidsbthr  14427  trilpo  14447  trirec0  14448  redcwlpo  14459  redc0  14461  dceqnconst  14463
  Copyright terms: Public domain W3C validator