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

Theorem eleq12d 2155
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 2154 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq1d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2153 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 186 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103   = 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-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  cbvraldva2  2589  cbvrexdva2  2590  cdeqel  2824  ru  2827  sbcel12g  2934  cbvralcsf  2977  cbvrexcsf  2978  cbvreucsf  2979  cbvrabcsf  2980  onintexmid  4354  elvvuni  4463  elrnmpt1  4647  smoeq  5990  smores  5992  smores2  5994  iordsmo  5997  nnaordi  6200  nnaordr  6202  ltapig  6818  ltmpig  6819  fzsubel  9382  elfzp1b  9418
  Copyright terms: Public domain W3C validator