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

Theorem ineq2i 3198
Description: Equality inference for intersection of two classes. (Contributed by NM, 26-Dec-1993.)
Hypothesis
Ref Expression
ineq1i.1  |-  A  =  B
Assertion
Ref Expression
ineq2i  |-  ( C  i^i  A )  =  ( C  i^i  B
)

Proof of Theorem ineq2i
StepHypRef Expression
1 ineq1i.1 . 2  |-  A  =  B
2 ineq2 3195 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2ax-mp 7 1  |-  ( C  i^i  A )  =  ( C  i^i  B
)
Colors of variables: wff set class
Syntax hints:    = wceq 1289    i^i cin 2998
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-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-in 3005
This theorem is referenced by:  in4  3216  inindir  3218  indif2  3243  difun1  3259  dfrab3ss  3277  dfif3  3406  intunsn  3726  rint0  3727  riin0  3801  res0  4717  resres  4725  resundi  4726  resindi  4728  inres  4730  resiun2  4733  resopab  4756  dfse2  4805  dminxp  4875  imainrect  4876  resdmres  4922  funimacnv  5090  unfiin  6636  sbthlemi5  6670  dmaddpi  6884  dmmulpi  6885  fsumiun  10871
  Copyright terms: Public domain W3C validator