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

Theorem ineq2d 3670
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 3664 . 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 1437    i^i cin 3441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449
This theorem is referenced by:  disjpr2  4065  rint0  4299  riin0  4376  disji2  4413  disjprg  4422  disjxun  4424  xpriindi  4991  riinint  5111  reseq2  5120  resindm  5169  predep  5425  onfr  5481  isofrlem  6246  isoselem  6247  oev2  7233  domss2  7737  funsnfsupp  7913  kmlem11  8588  fpwwe2cbv  9054  fpwwe2lem3  9057  fpwwe2lem8  9061  fpwwe2lem12  9065  fpwwe2lem13  9066  fpwwe2  9067  fz1isolem  12619  limsupgle  13513  fsumm1  13790  incexclem  13872  bitsinv1  14390  bitsinvp1  14397  sadcadd  14406  sadadd2  14408  smumullem  14440  ressbas  15141  ressress  15149  restval  15284  ismred2  15460  resscatc  15951  cnvps  16409  cntziinsn  16939  lsmdisj3r  17271  lsmdisj3b  17275  gsummptfzsplitl  17501  dmdprd  17565  subgdmdprd  17602  pgpfaclem1  17649  subrgpropd  17977  crng2idl  18398  obselocv  19222  basis1  19896  baspartn  19900  eltg  19903  tgdom  19925  indistopon  19947  ntrval  19982  clslp  20095  resttopon2  20115  restopnb  20122  paste  20241  nrmsep3  20302  imacmp  20343  cmpsub  20346  bwth  20356  llyi  20420  nllyi  20421  cldllycmp  20441  kgencmp2  20492  ptbasfi  20527  kqdisj  20678  kqcldsat  20679  trfbas2  20789  filss  20799  elfg  20817  flimclslem  20930  fcfneii  20983  tsmsfbas  21073  restutopopn  21184  ressxms  21471  restmetu  21516  qtopbaslem  21690  pi1addf  21971  pi1addval  21972  shftmbl  22369  voliunlem1  22380  voliunlem2  22381  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem4  22421  uniioombllem6  22423  volsup2  22440  volcn  22441  volivth  22442  itg1climres  22549  limciun  22726  dvres3a  22746  ig1pval  22998  2pthlem2  25171  frgrancvvdeqlem4  25606  issubgo  25876  omlsi  26892  pjoml  26924  chdmj3  27019  chdmj4  27020  ledi  27028  cmbr  27072  cmbr3  27096  pjoml3  27100  fh1  27106  fh2  27107  dmdbr  27787  dmdmd  27788  dmdbr5  27796  dmdsl3  27803  chirredlem2  27879  chirredlem3  27880  dmdbr6ati  27911  disji2f  28026  disjif2  28030  disjxpin  28037  disjunsn  28043  fimacnvinrn  28075  fimacnvinrn2  28076  prsss  28561  carsgclctunlem1  28978  carsgclctunlem2  28980  carsgclctunlem3  28981  ballotlemfval  29148  signsplypnf  29227  bnj1326  29623  mvrsval  29931  msrfval  29963  mthmpps  30008  dfpo2  30182  elima4  30208  topbnd  30765  opnbnd  30766  cldbnd  30767  neibastop1  30800  neibastop2lem  30801  neibastop2  30802  neibastop3  30803  neifg  30812  bj-diagval  31390  poimirlem3  31646  mblfinlem2  31681  ftc1anclem6  31725  heiborlem3  31848  pmodN  33123  polvalN  33178  polatN  33204  trnsetN  33430  djavalN  34411  dihmeetbclemN  34580  dihmeetlem11N  34593  djhval  34674  lclkrlem2e  34787  lcfrlem23  34841  lcdlss2N  34896  elrfi  35244  elrfirn  35245  elrfirn2  35246  eldioph2lem1  35310  conrel2d  35894  csbresgOLD  36855  inabs3  37036  disjiun2  37038  fresin2  37057  lptioo2  37282  lptioo1  37283  cncfuni  37335  fourierdlem48  37585  fourierdlem49  37586  fourierdlem93  37630  nnfoctbdjlem  37801  carageniuncllem1  37850  carageniuncllem2  37851  resisresindm  38381
  Copyright terms: Public domain W3C validator