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  2590  cbvrexdva2  2591  cdeqel  2825  ru  2828  sbcel12g  2935  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  onintexmid  4359  elvvuni  4468  elrnmpt1  4652  smoeq  6002  smores  6004  smores2  6006  iordsmo  6009  nnaordi  6212  nnaordr  6214  ltapig  6833  ltmpig  6834  fzsubel  9397  elfzp1b  9433
  Copyright terms: Public domain W3C validator