Theorem sseq2d 3979

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  sseq12d  3980  sseqtrd  3983  sbcrel  5743  funimass2  6599  fnssresb  6640  fnimaeq0  6651  foimacnv  6817  fvelimab  6933  ssimaexg  6947  ralima  7211  knatar  7332  frecseq123  8261  frrlem4  8268  onfununi  8310  oaordi  8510  oawordeulem  8518  oaass  8525  odi  8543  omass  8544  oen0  8550  oelim2  8559  nnaordi  8582  nnawordex  8601  naddunif  8657  pssnn  9132  fissuni  9308  dffi3  9382  cantnfle  9624  cantnflem1  9642  trcl  9681  r1sdom  9727  iscard2  9929  alephordi  10027  alephgeom  10035  cardaleph  10042  cardalephex  10043  ackbij2lem4  10194  cflm  10203  cfslbn  10220  cofsmo  10222  cfsmolem  10223  cfcoflem  10225  coftr  10226  alephsing  10229  fin23lem28  10293  fin23lem30  10295  fin23lem33  10298  fin1a2lem9  10361  axdc3lem2  10404  ttukeylem5  10466  pwfseqlem4a  10614  pwfseqlem4  10615  wunex2  10691  inar1  10728  sstskm  10795  fsuppmapnn0fiubex  13957  swrdnd  14619  swrd0  14623  repswswrd  14749  rtrclreclem1  15023  rtrclreclem2  15025  summolem2  15682  summo  15683  zsum  15684  sumz  15688  sumss  15690  fsumcvg3  15695  prodmolem2  15901  prodmo  15902  zprod  15903  prod1  15910  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  ramub2  16985  rami  16986  ramz2  16995  setsstruct2  17144  prdsval  17418  pwsle  17455  mrcuni  17582  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  eqgfval  19108  sscntz  19258  resscntz  19265  lsmlub  19594  efgrelexlemb  19680  efgcpbllemb  19685  gsumval3a  19833  gsumzaddlem  19851  gsumzoppg  19874  dmdprd  19930  dprdcntz  19940  subgdmdprd  19966  subrngpropd  20477  subrgpropd  20517  islss  20840  lsslss  20867  lsspropd  20924  lsmelpr  20998  lbspropd  21006  lsslinds  21740  ltbval  21950  opsrval  21953  mhpval  22026  isbasisg  22834  tgval  22842  tgss3  22873  restbas  23045  tgrest  23046  restcld  23059  restopn2  23064  restntr  23069  cnpnei  23151  cncls2  23160  perfcls  23252  cmpsublem  23286  cmpsub  23287  cmpcld  23289  uncmp  23290  hauscmplem  23293  cmpfi  23295  nconnsubb  23310  clsconn  23317  hausllycmp  23381  1stckgenlem  23440  txbas  23454  ptbasfi  23468  txcnpi  23495  ptcnp  23509  txcmplem1  23528  txcmplem2  23529  xkococnlem  23546  qtopcld  23600  fbasssin  23723  fbssint  23725  fbun  23727  fbasrn  23771  filufint  23807  ufinffr  23816  ufildr  23818  ustval  24090  trust  24117  elmopn  24330  neibl  24389  cfilucfil  24447  icccmplem1  24711  icccmplem2  24712  bndth  24857  isphtpc  24893  metcld  25206  bcthlem1  25224  bcth  25229  ovolfioo  25368  ovolficc  25369  elovolmr  25377  ovoliunlem3  25405  ovolicc2  25423  volsuplem  25456  dyadmax  25499  dyadmbllem  25500  dyadmbl  25501  precsexlem6  28114  precsexlem7  28115  incistruhgr  29006  edgssv2  29125  wksfval  29537  2wlkdlem9  29864  3wlkdlem9  30097  sspval  30652  ubth  30802  orthin  31375  chssoc  31425  chsscon3  31429  chsscon1  31430  h1datom  31511  pjoml6i  31518  osum  31574  spansncv  31582  pjcjt2  31621  pjopyth  31649  hstel2  32148  hstle  32159  stj  32164  dmdbr5  32237  mdslmd1lem1  32254  atord  32317  chirredlem4  32322  atcvat4i  32326  mdsymlem2  32333  mdsymlem3  32334  mdsymlem8  32339  padct  32643  ssnnssfz  32710  pwrssmgc  32926  lindspropd  33354  idlsrgval  33474  constr01  33732  constrmon  33734  constrextdg2lem  33738  constrextdg2  33739  constrfiss  33741  tpr2rico  33902  ordtrestNEW  33911  sigaval  34101  issiga  34102  issgon  34113  oms0  34288  omssubadd  34291  subgrwlk  35119  umgr2cycllem  35127  kur14  35203  cvmliftlem15  35285  satfsschain  35351  mclsrcl  35548  mclsval  35550  ivthALT  36323  isfne  36327  topfne  36342  neibastop3  36350  tailfb  36365  filnetlem1  36366  filnetlem4  36369  relowlssretop  37351  rdgssun  37366  poimirlem24  37638  mblfinlem2  37652  sstotbnd2  37768  sstotbnd  37769  sstotbnd3  37770  ssbnd  37782  cntotbnd  37790  cnpwstotbnd  37791  ismtyres  37802  heibor1lem  37803  heiborlem1  37805  heiborlem6  37810  heiborlem8  37812  exidreslem  37871  scottexf  38162  scott0f  38163  cnvref4  38332  dfrefrels2  38504  dfrefrel2  38506  lshpcmp  38981  lsmsat  39001  lsmsatcv  39003  lfl1dim  39114  lfl1dim2N  39115  lkrss2N  39162  psubspset  39738  paddss  39839  psubclsetN  39930  dilfsetN  40146  dilsetN  40147  diaglbN  41049  dibglbN  41160  dihlspsnat  41327  dihglb2  41336  dochffval  41343  dochfval  41344  dochvalr  41351  dochord2N  41365  dochsncom  41376  dihjat1lem  41422  dvh4dimat  41432  dvh3dimatN  41433  dvh2dimatN  41434  dochexmidlem1  41454  lpolsetN  41476  lpolconN  41481  hdmaplkr  41907  hdmapoc  41925  hlhillcs  41952  ismrc  42689  incssnn0  42699  nacsfix  42700  hbt  43119  oacl2g  43319  omcl2  43322  ofoaf  43344  naddwordnexlem4  43390  ss2iundf  43648  clsk1indlem1  44034  clsk1independent  44035  isotone1  44037  isotone2  44038  ntrclsiso  44056  ntrclsk2  44057  scottelrankd  44236  ssinc  45081  uzfissfz  45322  stoweidlem50  46048  stoweidlem57  46055  fourierdlem20  46125  fourierdlem50  46154  fourierdlem64  46168  fourierdlem86  46190  fourierdlem103  46207  fourierdlem104  46208  ovnval  46539  hoicvrrex  46554  ovnlecvr  46556  ovncvrrp  46562  ovnsubaddlem1  46568  hoidmvlelem3  46595  hoidmvle  46598  ovnhoilem1  46599  ovnhoi  46601  ovnlecvr2  46608  ovncvr2  46609  hspmbl  46627  ovolval4lem2  46648  ovolval5lem2  46651  ovolval5lem3  46652  ovolval5  46653  ovnovollem1  46654  ovnovollem2  46655  sprsymrelfvlem  47491  grlimgrtri  47995  grilcbri2  48003  uspgrsprf  48134  uspgrsprfo  48136  ssnn0ssfz  48337  lincfsuppcl  48402  iunlub  48809  lubeldm2d  48946  glbeldm2d  48947