MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ineq2d Structured version   Visualization version   Unicode version

Theorem ineq2d 3602
Description: Equality deduction for intersection of two classes. (Contributed by NM, 10-Apr-1994.)
Hypothesis
Ref Expression
ineq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
ineq2d  |-  ( ph  ->  ( C  i^i  A
)  =  ( C  i^i  B ) )

Proof of Theorem ineq2d
StepHypRef Expression
1 ineq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ineq2 3596 . 2  |-  ( A  =  B  ->  ( C  i^i  A )  =  ( C  i^i  B
) )
31, 2syl 17 1  |-  ( ph  ->  ( C  i^i  A
)  =  ( C  i^i  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1448    i^i cin 3371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-in 3379
This theorem is referenced by:  disjpr2  4002  rint0  4245  riin0  4322  disji2  4361  disjprg  4370  disjxun  4372  xpriindi  4949  riinint  5069  reseq2  5078  resindm  5127  predep  5385  onfr  5441  isofrlem  6217  isoselem  6218  oev2  7212  domss2  7718  funsnfsupp  7894  kmlem11  8577  fpwwe2cbv  9042  fpwwe2lem3  9045  fpwwe2lem8  9049  fpwwe2lem12  9053  fpwwe2lem13  9054  fpwwe2  9055  fz1isolem  12619  limsupgle  13546  fsumm1  13823  incexclem  13905  bitsinv1  14427  bitsinvp1  14434  sadcadd  14443  sadadd2  14445  smumullem  14477  ressbas  15190  ressress  15198  restval  15336  ismred2  15520  resscatc  16011  cnvps  16469  cntziinsn  16999  lsmdisj3r  17347  lsmdisj3b  17351  gsummptfzsplitl  17577  dmdprd  17641  subgdmdprd  17678  pgpfaclem1  17725  subrgpropd  18053  crng2idl  18474  obselocv  19302  basis1  19976  baspartn  19980  eltg  19983  tgdom  20005  indistopon  20027  ntrval  20062  clslp  20175  resttopon2  20195  restopnb  20202  paste  20321  nrmsep3  20382  imacmp  20423  cmpsub  20426  bwth  20436  llyi  20500  nllyi  20501  cldllycmp  20521  kgencmp2  20572  ptbasfi  20607  kqdisj  20758  kqcldsat  20759  trfbas2  20869  filss  20879  elfg  20897  flimclslem  21010  fcfneii  21063  tsmsfbas  21153  restutopopn  21264  ressxms  21551  restmetu  21596  qtopbaslem  21790  pi1addf  22089  pi1addval  22090  shftmbl  22503  voliunlem1  22515  voliunlem2  22516  uniioombllem2  22552  uniioombllem2OLD  22553  uniioombllem4  22556  uniioombllem6  22558  volsup2  22575  volcn  22576  volivth  22577  itg1climres  22684  limciun  22861  dvres3a  22881  ig1pval  23136  ig1pvalOLD  23142  2pthlem2  25338  frgrancvvdeqlem4  25773  issubgo  26043  omlsi  27069  pjoml  27101  chdmj3  27196  chdmj4  27197  ledi  27205  cmbr  27249  cmbr3  27273  pjoml3  27277  fh1  27283  fh2  27284  dmdbr  27964  dmdmd  27965  dmdbr5  27973  dmdsl3  27980  chirredlem2  28056  chirredlem3  28057  dmdbr6ati  28088  disji2f  28197  disjif2  28201  disjxpin  28208  disjunsn  28214  fimacnvinrn  28244  fimacnvinrn2  28245  prsss  28729  carsgclctunlem1  29155  carsgclctunlem2  29157  carsgclctunlem3  29158  ballotlemfval  29328  signsplypnf  29445  bnj1326  29841  mvrsval  30149  msrfval  30181  mthmpps  30226  dfpo2  30401  elima4  30427  topbnd  30986  opnbnd  30987  cldbnd  30988  neibastop1  31021  neibastop2lem  31022  neibastop2  31023  neibastop3  31024  neifg  31033  bj-diagval  31647  csbpredg  31729  poimirlem3  31945  mblfinlem2  31980  ftc1anclem6  32024  heiborlem3  32147  pmodN  33417  polvalN  33472  polatN  33498  trnsetN  33724  djavalN  34705  dihmeetbclemN  34874  dihmeetlem11N  34887  djhval  34968  lclkrlem2e  35081  lcfrlem23  35135  lcdlss2N  35190  elrfi  35538  elrfirn  35539  elrfirn2  35540  eldioph2lem1  35604  conrel2d  36258  csbresgOLD  37213  inabs3  37391  disjiun2  37393  fresin2  37446  lptioo2  37753  lptioo1  37754  cncfuni  37806  fourierdlem48  38075  fourierdlem49  38076  fourierdlem93  38120  qndenserrnbllem  38220  nnfoctbdjlem  38354  carageniuncllem1  38406  carageniuncllem2  38407  hoiqssbllem3  38509  resisresindm  39103  pthdlem2  39846
  Copyright terms: Public domain W3C validator