Theorem sseq2d 4014

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 4008	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  sseq12d  4015  sseqtrd  4022  sbcrel  5780  funimass2  6631  fncoOLD  6668  fnssresb  6672  fnimaeq0  6683  foimacnv  6850  fvelimab  6964  ssimaexg  6977  knatar  7357  frecseq123  8273  frrlem4  8280  wfrdmclOLD  8323  wfrlem12OLD  8326  onfununi  8347  oaordi  8552  oawordeulem  8560  oaass  8567  odi  8585  omass  8586  oen0  8592  oelim2  8601  nnaordi  8624  nnawordex  8643  naddunif  8698  pssnn  9174  pssnnOLD  9271  fissuni  9363  dffi3  9432  cantnfle  9672  cantnflem1  9690  trcl  9729  r1sdom  9775  iscard2  9977  alephordi  10075  alephgeom  10083  cardaleph  10090  cardalephex  10091  ackbij2lem4  10243  cflm  10251  cfslbn  10268  cofsmo  10270  cfsmolem  10271  cfcoflem  10273  coftr  10274  alephsing  10277  fin23lem28  10341  fin23lem30  10343  fin23lem33  10346  fin1a2lem9  10409  axdc3lem2  10452  ttukeylem5  10514  fpwwe2lem4  10635  pwfseqlem4a  10662  pwfseqlem4  10663  wunex2  10739  inar1  10776  sstskm  10843  fsuppmapnn0fiubex  13964  swrdnd  14611  swrd0  14615  repswswrd  14741  rtrclreclem1  15011  rtrclreclem2  15013  summolem2  15669  summo  15670  zsum  15671  sumz  15675  sumss  15677  fsumcvg3  15682  prodmolem2  15886  prodmo  15887  zprod  15888  prod1  15895  vdwlem1  16921  vdwlem12  16932  vdwlem13  16933  ramub2  16954  rami  16955  ramz2  16964  setsstruct2  17114  prdsval  17408  pwsle  17445  mrcuni  17572  gsumpropd  18609  gsumpropd2lem  18610  gsumress  18613  eqgfval  19099  sscntz  19238  resscntz  19245  lsmlub  19580  efgrelexlemb  19666  efgcpbllemb  19671  gsumval3a  19819  gsumzaddlem  19837  gsumzoppg  19860  dmdprd  19916  dprdcntz  19926  subgdmdprd  19952  subrngpropd  20464  subrgpropd  20506  islss  20777  lsslss  20804  lsspropd  20861  lsmelpr  20935  lbspropd  20943  lsslinds  21696  ltbval  21909  opsrval  21912  mhpval  21992  isbasisg  22770  tgval  22778  tgss3  22809  restbas  22982  tgrest  22983  restcld  22996  restopn2  23001  restntr  23006  cnpnei  23088  cncls2  23097  perfcls  23189  cmpsublem  23223  cmpsub  23224  cmpcld  23226  uncmp  23227  hauscmplem  23230  cmpfi  23232  nconnsubb  23247  clsconn  23254  hausllycmp  23318  1stckgenlem  23377  txbas  23391  ptbasfi  23405  txcnpi  23432  ptcnp  23446  txcmplem1  23465  txcmplem2  23466  xkococnlem  23483  qtopcld  23537  fbasssin  23660  fbssint  23662  fbun  23664  fbasrn  23708  filufint  23744  ufinffr  23753  ufildr  23755  ustval  24027  trust  24054  elmopn  24268  neibl  24330  cfilucfil  24388  icccmplem1  24658  icccmplem2  24659  bndth  24804  isphtpc  24840  metcld  25154  bcthlem1  25172  bcth  25177  ovolfioo  25316  ovolficc  25317  elovolmr  25325  ovoliunlem3  25353  ovolicc2  25371  volsuplem  25404  dyadmax  25447  dyadmbllem  25448  dyadmbl  25449  precsexlem6  28023  precsexlem7  28024  incistruhgr  28772  edgssv2  28888  wksfval  29299  2wlkdlem9  29621  3wlkdlem9  29854  sspval  30409  ubth  30559  orthin  31132  chssoc  31182  chsscon3  31186  chsscon1  31187  h1datom  31268  pjoml6i  31275  osum  31331  spansncv  31339  pjcjt2  31378  pjopyth  31406  hstel2  31905  hstle  31916  stj  31921  dmdbr5  31994  mdslmd1lem1  32011  atord  32074  chirredlem4  32079  atcvat4i  32083  mdsymlem2  32090  mdsymlem3  32091  mdsymlem8  32096  padct  32377  ssnnssfz  32431  pwrssmgc  32603  lindspropd  32939  idlsrgval  33057  tpr2rico  33356  ordtrestNEW  33365  sigaval  33573  issiga  33574  issgon  33585  oms0  33760  omssubadd  33763  subgrwlk  34587  umgr2cycllem  34595  kur14  34671  cvmliftlem15  34753  satfsschain  34819  mclsrcl  35016  mclsval  35018  ivthALT  35684  isfne  35688  topfne  35703  neibastop3  35711  tailfb  35726  filnetlem1  35727  filnetlem4  35730  relowlssretop  36708  rdgssun  36723  poimirlem24  36976  mblfinlem2  36990  sstotbnd2  37106  sstotbnd  37107  sstotbnd3  37108  ssbnd  37120  cntotbnd  37128  cnpwstotbnd  37129  ismtyres  37140  heibor1lem  37141  heiborlem1  37143  heiborlem6  37148  heiborlem8  37150  exidreslem  37209  scottexf  37500  scott0f  37501  cnvref4  37683  dfrefrels2  37847  dfrefrel2  37849  lshpcmp  38322  lsmsat  38342  lsmsatcv  38344  lfl1dim  38455  lfl1dim2N  38456  lkrss2N  38503  psubspset  39079  paddss  39180  psubclsetN  39271  dilfsetN  39487  dilsetN  39488  diaglbN  40390  dibglbN  40501  dihlspsnat  40668  dihglb2  40677  dochffval  40684  dochfval  40685  dochvalr  40692  dochord2N  40706  dochsncom  40717  dihjat1lem  40763  dvh4dimat  40773  dvh3dimatN  40774  dvh2dimatN  40775  dochexmidlem1  40795  lpolsetN  40817  lpolconN  40822  hdmaplkr  41248  hdmapoc  41266  hlhillcs  41297  ismrc  41902  incssnn0  41912  nacsfix  41913  hbt  42335  oacl2g  42543  omcl2  42546  ofoaf  42568  naddwordnexlem4  42615  ss2iundf  42873  clsk1indlem1  43259  clsk1independent  43260  isotone1  43262  isotone2  43263  ntrclsiso  43281  ntrclsk2  43282  scottelrankd  43469  ssinc  44238  uzfissfz  44495  stoweidlem50  45225  stoweidlem57  45232  fourierdlem20  45302  fourierdlem50  45331  fourierdlem64  45345  fourierdlem86  45367  fourierdlem103  45384  fourierdlem104  45385  ovnval  45716  hoicvrrex  45731  ovnlecvr  45733  ovncvrrp  45739  ovnsubaddlem1  45745  hoidmvlelem3  45772  hoidmvle  45775  ovnhoilem1  45776  ovnhoi  45778  ovnlecvr2  45785  ovncvr2  45786  hspmbl  45804  ovolval4lem2  45825  ovolval5lem2  45828  ovolval5lem3  45829  ovolval5  45830  ovnovollem1  45831  ovnovollem2  45832  sprsymrelfvlem  46617  uspgrsprf  46983  uspgrsprfo  46985  ssnn0ssfz  47188  lincfsuppcl  47256  lubeldm2d  47753  glbeldm2d  47754