Theorem sseq2d 3596

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq2d	⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq2 3590	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseq12d  3597  sseqtrd  3604  sbcrel  5128  funimass2  5886  fnco  5913  fnssresb  5917  fnimaeq0  5926  foimacnv  6067  fvelimab  6163  ssimaexg  6174  knatar  6507  wfrdmcl  7310  wfrlem12  7313  onfununi  7325  oaordi  7513  oawordeulem  7521  oaass  7528  odi  7546  omass  7547  oen0  7553  oelim2  7562  nnaordi  7585  nnawordex  7604  pssnn  8063  fissuni  8154  dffi3  8220  cantnfle  8451  cantnflem1  8469  trcl  8487  r1sdom  8520  iscard2  8685  alephordi  8780  alephgeom  8788  cardaleph  8795  cardalephex  8796  ackbij2lem4  8947  cflm  8955  cfslbn  8972  cofsmo  8974  cfsmolem  8975  cfcoflem  8977  coftr  8978  alephsing  8981  fin23lem28  9045  fin23lem30  9047  fin23lem33  9050  fin1a2lem9  9113  axdc3lem2  9156  ttukeylem5  9218  fpwwe2lem5  9335  pwfseqlem4a  9362  pwfseqlem4  9363  wunex2  9439  inar1  9476  sstskm  9543  fsuppmapnn0fiubex  12654  swrdnd  13284  swrd0  13286  repswswrd  13382  rtrclreclem1  13646  rtrclreclem2  13647  summolem2  14294  summo  14295  zsum  14296  sumz  14300  sumss  14302  fsumcvg3  14307  prodmolem2  14504  prodmo  14505  zprod  14506  prod1  14513  vdwlem1  15523  vdwlem12  15534  vdwlem13  15535  ramub2  15556  rami  15557  ramz2  15566  prdsval  15938  pwsle  15975  mrcuni  16104  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  eqgfval  17465  sscntz  17582  resscntz  17587  lsmlub  17901  efgrelexlemb  17986  efgcpbllemb  17991  gsumval3a  18127  gsumzaddlem  18144  gsumzoppg  18167  dmdprd  18220  dprdcntz  18230  subgdmdprd  18256  subrgpropd  18637  islss  18756  lsslss  18782  lsspropd  18838  lsmelpr  18912  lbspropd  18920  ltbval  19292  opsrval  19295  lsslinds  19989  isbasisg  20562  tgval  20570  tgss3  20601  restbas  20772  tgrest  20773  restcld  20786  restopn2  20791  restntr  20796  cnpnei  20878  cncls2  20887  perfcls  20979  cmpsublem  21012  cmpsub  21013  cmpcld  21015  uncmp  21016  hauscmplem  21019  cmpfi  21021  nconsubb  21036  clscon  21043  hausllycmp  21107  1stckgenlem  21166  txbas  21180  ptbasfi  21194  txcnpi  21221  ptcnp  21235  txcmplem1  21254  txcmplem2  21255  xkococnlem  21272  qtopcld  21326  fbasssin  21450  fbssint  21452  fbun  21454  fbasrn  21498  filufint  21534  ufinffr  21543  ufildr  21545  ustval  21816  trust  21843  elmopn  22057  neibl  22116  cfilucfil  22174  icccmplem1  22433  icccmplem2  22434  bndth  22565  isphtpc  22601  metcld  22912  bcthlem1  22929  bcth  22934  ovolfioo  23043  ovolficc  23044  elovolmr  23051  ovoliunlem3  23079  ovolicc2  23097  volsuplem  23130  dyadmax  23172  dyadmbllem  23173  dyadmbl  23174  structvtxvallem  25697  incistruhgr  25746  isfrgra  26517  sspval  26962  ubth  27113  orthin  27689  chssoc  27739  chsscon3  27743  chsscon1  27744  h1datom  27825  pjoml6i  27832  osum  27888  spansncv  27896  pjcjt2  27935  pjopyth  27963  hstel2  28462  hstle  28473  stj  28478  dmdbr5  28551  mdslmd1lem1  28568  atord  28631  chirredlem4  28636  atcvat4i  28640  mdsymlem2  28647  mdsymlem3  28648  mdsymlem8  28653  padct  28885  ssnnssfz  28937  tpr2rico  29286  ordtrestNEW  29295  sigaval  29500  issiga  29501  issgon  29513  oms0  29686  omssubadd  29689  kur14  30452  cvmliftlem15  30534  mclsrcl  30712  mclsval  30714  trpredtr  30974  dftrpred3g  30977  frrlem5e  31032  nofulllem1  31101  nofulllem2  31102  ivthALT  31500  isfne  31504  topfne  31519  neibastop3  31527  tailfb  31542  filnetlem1  31543  filnetlem4  31546  csbwrecsg  32349  relowlssretop  32387  poimirlem24  32603  mblfinlem2  32617  sstotbnd2  32743  sstotbnd  32744  sstotbnd3  32745  ssbnd  32757  cntotbnd  32765  cnpwstotbnd  32766  ismtyres  32777  heibor1lem  32778  heiborlem1  32780  heiborlem6  32785  heiborlem8  32787  exidreslem  32846  scottexf  33146  scott0f  33147  lshpcmp  33293  lsmsat  33313  lsmsatcv  33315  lfl1dim  33426  lfl1dim2N  33427  lkrss2N  33474  psubspset  34048  paddss  34149  psubclsetN  34240  dilfsetN  34457  dilsetN  34458  diaglbN  35362  dibglbN  35473  dihlspsnat  35640  dihglb2  35649  dochffval  35656  dochfval  35657  dochvalr  35664  dochord2N  35678  dochsncom  35689  dihjat1lem  35735  dvh4dimat  35745  dvh3dimatN  35746  dvh2dimatN  35747  dochexmidlem1  35767  lpolsetN  35789  lpolconN  35794  hdmaplkr  36223  hdmapoc  36241  hlhillcs  36268  ismrc  36282  incssnn0  36292  nacsfix  36293  hbt  36719  ss2iundf  36970  clsk1indlem1  37363  clsk1independent  37364  isotone1  37366  isotone2  37367  ntrclsiso  37385  ntrclsk2  37386  ssinc  38292  uzfissfz  38483  stoweidlem50  38943  stoweidlem57  38950  fourierdlem20  39020  fourierdlem50  39049  fourierdlem64  39063  fourierdlem86  39085  fourierdlem103  39102  fourierdlem104  39103  ovnval  39431  hoicvrrex  39446  ovnlecvr  39448  ovncvrrp  39454  ovnsubaddlem1  39460  hoidmvlelem3  39487  hoidmvle  39490  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  ovncvr2  39501  hspmbl  39519  ovolval4lem2  39540  ovolval5lem2  39543  ovolval5lem3  39544  ovolval5  39545  ovnovollem1  39546  ovnovollem2  39547  edgassv2  40425  1wlksfval  40811  21wlkdlem9  41141  31wlkdlem9  41335  isfrgr  41430  ssnn0ssfz  41920  lincfsuppcl  41996