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

Theorem eqeq1 2062
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 2050 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 117 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1466 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43bibi1d 226 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
54albidv 1721 . 2 (𝐴 = 𝐵 → (∀𝑥(𝑥𝐴𝑥𝐶) ↔ ∀𝑥(𝑥𝐵𝑥𝐶)))
6 dfcleq 2050 . 2 (𝐴 = 𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
7 dfcleq 2050 . 2 (𝐵 = 𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
85, 6, 73bitr4g 216 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102  wal 1257   = wceq 1259  wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  eqeq1i  2063  eqeq1d  2064  eqeq2  2065  eqeq12  2068  eqtr  2073  eqsb3lem  2156  clelab  2178  neeq1  2233  pm13.18  2301  issetf  2579  sbhypf  2620  vtoclgft  2621  eqvincf  2692  pm13.183  2704  eueq  2735  mob  2746  euind  2751  reuind  2767  eqsbc3  2825  csbhypf  2913  uniiunlem  3056  snjust  3408  elsng  3418  elprg  3423  rabrsndc  3466  sneqrg  3561  preq12bg  3572  intab  3672  dfiin2g  3718  opthg  4003  copsexg  4009  euotd  4019  elopab  4023  snnex  4209  uniuni  4211  eusv1  4212  reusv3  4220  ordtriexmid  4275  onsucelsucexmidlem1  4281  onsucelsucexmid  4283  regexmidlemm  4285  regexmidlem1  4286  reg2exmidlema  4287  wetriext  4329  nn0suc  4355  nndceq0  4367  0elnn  4368  elxpi  4389  opbrop  4447  relop  4514  ideqg  4515  elrnmpt  4611  elrnmpt1  4613  elrnmptg  4614  cnveqb  4804  relcoi1  4877  funopg  4962  funcnvuni  4996  fun11iun  5175  fvelrnb  5249  fvmptg  5276  fndmin  5302  eldmrexrn  5336  foelrn  5345  foco2  5346  fmptco  5358  elabrex  5425  abrexco  5426  f1veqaeq  5436  f1oiso  5493  eusvobj2  5526  acexmidlema  5531  acexmidlemb  5532  acexmidlem2  5537  acexmidlemv  5538  oprabid  5565  mpt2fun  5631  elrnmpt2g  5641  elrnmpt2  5642  ralrnmpt2  5643  rexrnmpt2  5644  ovi3  5665  ov6g  5666  ovelrn  5677  caovcang  5690  caovcan  5693  eloprabi  5850  dftpos4  5909  elqsg  6187  qsel  6214  brecop  6227  eroveu  6228  erovlem  6229  th3qlem1  6239  th3q  6242  2dom  6316  fundmen  6317  nneneq  6351  supsnti  6409  isotilem  6410  indpi  6498  nqtri3or  6552  enq0sym  6588  enq0ref  6589  enq0tr  6590  enq0breq  6592  addnq0mo  6603  mulnq0mo  6604  mulnnnq0  6606  genipv  6665  genpelvl  6668  genpelvu  6669  addsrmo  6886  mulsrmo  6887  aptisr  6921  ltresr  6973  axcnre  7013  axpre-apti  7017  apreap  7652  apreim  7668  creur  7987  creui  7988  nn1m1nn  8008  nn1gt1  8023  elz  8304  nn0ind-raph  8414  nltpnft  8831  xnegeq  8841  flqeqceilz  9268  expival  9422  shftfvalg  9647  shftfval  9650  ndvdssub  10242  bj-nn0suc0  10462  bj-inf2vnlem1  10482  bj-inf2vnlem2  10483  bj-nn0sucALT  10490
  Copyright terms: Public domain W3C validator