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

Theorem eleq12d 2241
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq1d.1 (𝜑𝐴 = 𝐵)
eleq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
eleq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3 (𝜑𝐶 = 𝐷)
21eleq2d 2240 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq1d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2239 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 187 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104   = wceq 1348  wcel 2141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166
This theorem is referenced by:  cbvraldva2  2703  cbvrexdva2  2704  cdeqel  2951  ru  2954  sbcel12g  3064  cbvralcsf  3111  cbvrexcsf  3112  cbvreucsf  3113  cbvrabcsf  3114  onintexmid  4555  elvvuni  4673  elrnmpt1  4860  canth  5804  smoeq  6266  smores  6268  smores2  6270  iordsmo  6273  nnaordi  6484  nnaordr  6486  fvixp  6677  cbvixp  6689  mptelixpg  6708  exmidaclem  7172  cc1  7214  cc2lem  7215  cc3  7217  ltapig  7287  ltmpig  7288  fzsubel  10003  elfzp1b  10040  ennnfonelemg  12345  ennnfonelemp1  12348  ennnfonelemnn0  12364  ctiunctlemu1st  12376  ctiunctlemu2nd  12377  ctiunctlemudc  12379  ctiunctlemfo  12381  ismgm  12598  mgm1  12611  ismndd  12660  istps  12783  tpspropd  12787  eltpsg  12791  isms  13206  mspropd  13231  cnlimci  13395
  Copyright terms: Public domain W3C validator