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

Theorem ineq2d 3243
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ineq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem ineq2d
StepHypRef Expression
1 ineq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ineq2 3237 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 14 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  cin 3036
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-v 2659  df-in 3043
This theorem is referenced by:  disjpr2  3553  rint0  3776  riin0  3850  disji2  3888  xpriindim  4637  riinint  4758  reseq2  4772  csbresg  4780  resindm  4819  isoselem  5675  zfz1isolem1  10476  fsumm1  11077  ennnfonelemhf1o  11771  restval  11969  basis1  12057  baspartn  12060  eltg  12064  tgdom  12084  ntrval  12122  resttopon2  12190  restopnb  12193  qtopbasss  12510
  Copyright terms: Public domain W3C validator