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

Theorem eqeq1 2091
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 2079 . . . . . 6 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
21biimpi 118 . . . . 5 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
3219.21bi 1493 . . . 4 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
43bibi1d 231 . . 3 (𝐴 = 𝐵 → ((𝑥𝐴𝑥𝐶) ↔ (𝑥𝐵𝑥𝐶)))
54albidv 1749 . 2 (𝐴 = 𝐵 → (∀𝑥(𝑥𝐴𝑥𝐶) ↔ ∀𝑥(𝑥𝐵𝑥𝐶)))
6 dfcleq 2079 . 2 (𝐴 = 𝐶 ↔ ∀𝑥(𝑥𝐴𝑥𝐶))
7 dfcleq 2079 . 2 (𝐵 = 𝐶 ↔ ∀𝑥(𝑥𝐵𝑥𝐶))
85, 6, 73bitr4g 221 1 (𝐴 = 𝐵 → (𝐴 = 𝐶𝐵 = 𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1285   = wceq 1287  wcel 1436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  eqeq1i  2092  eqeq1d  2093  eqeq2  2094  eqeq12  2097  eqtr  2102  eqsb3lem  2187  clelab  2209  neeq1  2264  pm13.18  2332  issetf  2620  sbhypf  2662  vtoclgft  2663  eqvincf  2733  pm13.183  2745  eueq  2777  mob  2788  euind  2793  reuind  2809  eqsbc3  2867  csbhypf  2955  uniiunlem  3098  snjust  3436  elsng  3446  elprg  3451  rabrsndc  3493  sneqrg  3589  preq12bg  3600  intab  3700  dfiin2g  3746  opthg  4039  copsexg  4045  euotd  4055  elopab  4059  snnex  4245  uniuni  4247  eusv1  4248  reusv3  4256  ordtriexmid  4311  onsucelsucexmidlem1  4317  onsucelsucexmid  4319  regexmidlemm  4321  regexmidlem1  4322  reg2exmidlema  4323  wetriext  4365  nn0suc  4392  nndceq0  4404  0elnn  4405  elxpi  4427  opbrop  4485  relop  4554  ideqg  4555  elrnmpt  4652  elrnmpt1  4654  elrnmptg  4655  cnveqb  4852  relcoi1  4928  funopg  5013  funcnvuni  5048  f0rn0  5168  fun11iun  5237  fvelrnb  5315  fvmptg  5343  fndmin  5369  eldmrexrn  5403  fmptco  5427  foelrnOLD  5493  foco2  5494  elabrex  5498  abrexco  5499  f1veqaeq  5509  f1oiso  5566  eusvobj2  5599  acexmidlema  5604  acexmidlemb  5605  acexmidlem2  5610  acexmidlemv  5611  oprabid  5638  mpt2fun  5704  elrnmpt2g  5714  elrnmpt2  5715  ralrnmpt2  5716  rexrnmpt2  5717  ovi3  5738  ov6g  5739  ovelrn  5750  caovcang  5763  caovcan  5766  eloprabi  5923  dftpos4  5982  tfr1onlemaccex  6067  tfrcllemaccex  6080  elqsg  6294  qsel  6321  brecop  6334  eroveu  6335  erovlem  6336  th3qlem1  6346  th3q  6349  2dom  6474  fundmen  6475  xpf1o  6512  nneneq  6525  tridc  6567  fisseneq  6592  supsnti  6644  isotilem  6645  updjudhcoinrg  6716  updjud  6717  indpi  6845  nqtri3or  6899  enq0sym  6935  enq0ref  6936  enq0tr  6937  enq0breq  6939  addnq0mo  6950  mulnq0mo  6951  mulnnnq0  6953  genipv  7012  genpelvl  7015  genpelvu  7016  addsrmo  7233  mulsrmo  7234  aptisr  7268  ltresr  7320  axcnre  7360  axpre-apti  7364  apreap  8005  apreim  8021  creur  8354  creui  8355  nn1m1nn  8375  nn1gt1  8390  elz  8685  nn0ind-raph  8796  nltpnft  9211  xnegeq  9221  flqeqceilz  9653  1tonninf  9774  iseqf1olemqval  9820  iseqf1olemqk  9827  iseqf1olemqsum  9833  expival  9855  shftfvalg  10148  shftfval  10151  isummo  10662  fisum  10665  ndvdssub  10805  gcdval  10826  bezoutlemnewy  10860  bezoutlema  10863  bezoutlemb  10864  lcmval  10920  coprmgcdb  10945  coprmdvds1  10948  divgcdcoprmex  10959  dvdsprime  10979  nprm  10980  dvdsprm  10993  coprm  10998  qnumval  11038  qdenval  11039  bj-nn0suc0  11283  bj-inf2vnlem1  11303  bj-inf2vnlem2  11304  bj-nn0sucALT  11311  nnsf  11333  peano3nninf  11335  nninfall  11338  exmidsbthr  11351
  Copyright terms: Public domain W3C validator