Theorem sseq2d 3972

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  sseq12d  3973  sseqtrd  3976  sbcrel  5772  funimass2  6626  fnssresb  6664  fnimaeq0  6675  foimacnv  6845  fvelimab  6960  ssimaexg  6974  ralima  7242  knatar  7368  frecseq123  8288  frrlem4  8295  onfununi  8337  oaordi  8540  oawordeulem  8548  oaass  8555  odi  8573  omass  8574  oen0  8581  oelim2  8590  nnaordi  8613  nnawordex  8632  naddunif  8689  pssnn  9163  fissuni  9324  dffi3  9401  cantnfle  9650  cantnflem1  9668  trcl  9707  r1sdom  9756  scottex  9872  scottelrankd  9887  iscard2  9981  alephordi  10077  alephgeom  10085  cardaleph  10092  cardalephex  10093  ackbij2lem4  10243  cflm  10251  cfslbn  10269  cofsmo  10271  cfsmolem  10272  cfcoflem  10274  coftr  10275  alephsing  10278  fin23lem28  10342  fin23lem30  10344  fin23lem33  10347  fin1a2lem9  10410  axdc3lem2  10453  ttukeylem5  10515  pwfseqlem4a  10664  pwfseqlem4  10665  wunex2  10741  inar1  10778  sstskm  10845  fsuppmapnn0fiubex  14048  swrdnd  14716  swrd0  14720  repswswrd  14847  rtrclreclem1  15120  rtrclreclem2  15122  summolem2  15793  summo  15794  zsum  15795  sumz  15799  sumss  15801  fsumcvg3  15806  prodmolem2  16015  prodmo  16016  zprod  16017  prod1  16024  vdwlem1  17066  vdwlem12  17077  vdwlem13  17078  ramub2  17099  rami  17100  ramz2  17109  setsstruct2  17259  prdsval  17533  pwsle  17571  mrcuni  17702  gsumpropd  18765  gsumpropd2lem  18766  gsumress  18769  eqgfval  19275  sscntz  19427  resscntz  19434  lsmlub  19765  efgrelexlemb  19851  efgcpbllemb  19856  gsumval3a  20004  gsumzaddlem  20022  gsumzoppg  20045  dmdprd  20101  dprdcntz  20111  subgdmdprd  20137  subrngpropd  20704  subrgpropd  20744  islss  21092  lsslss  21119  lsspropd  21175  lsmelpr  21249  lbspropd  21257  lsslinds  22018  ltbval  22231  opsrval  22234  mhpval  22339  isbasisg  23141  tgval  23149  tgss3  23180  restbas  23352  tgrest  23353  restcld  23366  restopn2  23371  restntr  23376  cnpnei  23458  cncls2  23467  perfcls  23559  cmpsublem  23593  cmpsub  23594  cmpcld  23596  uncmp  23597  hauscmplem  23600  cmpfi  23602  nconnsubb  23617  clsconn  23624  hausllycmp  23688  1stckgenlem  23747  txbas  23761  ptbasfi  23775  txcnpi  23802  ptcnp  23816  txcmplem1  23835  txcmplem2  23836  xkococnlem  23853  qtopcld  23907  fbasssin  24030  fbssint  24032  fbun  24034  fbasrn  24078  filufint  24114  ufinffr  24123  ufildr  24125  ustval  24397  trust  24423  elmopn  24636  neibl  24695  cfilucfil  24753  icccmplem1  25017  icccmplem2  25018  bndth  25154  isphtpc  25190  metcld  25502  bcthlem1  25520  bcth  25525  ovolfioo  25663  ovolficc  25664  elovolmr  25672  ovoliunlem3  25700  ovolicc2  25718  volsuplem  25751  dyadmax  25794  dyadmbllem  25795  dyadmbl  25796  precsexlem6  28442  precsexlem7  28443  bdayfinbndlem1  28697  bdayfinbndlem2  28698  lnssplng  29111  incistruhgr  29466  edgssv2  29585  wksfval  29996  2wlkdlem9  30320  3wlkdlem9  30556  sspval  31112  ubth  31262  orthin  31835  chssoc  31885  chsscon3  31889  chsscon1  31890  h1datom  31971  pjoml6i  31978  osum  32034  spansncv  32042  pjcjt2  32081  pjopyth  32109  hstel2  32608  hstle  32619  stj  32624  dmdbr5  32697  mdslmd1lem1  32714  atord  32777  chirredlem4  32782  atcvat4i  32786  mdsymlem2  32793  mdsymlem3  32794  mdsymlem8  32799  padct  33100  ssnnssfz  33169  pwrssmgc  33351  lindspropd  33727  idlsrgval  33824  constr01  34163  constrmon  34165  constrextdg2lem  34169  constrextdg2  34170  constrfiss  34172  tpr2rico  34333  ordtrestNEW  34342  sigaval  34532  issiga  34533  issgon  34544  oms0  34718  omssubadd  34721  elscottrankss  35540  subgrwlk  35644  umgr2cycllem  35652  kur14  35728  cvmliftlem15  35810  satfsschain  35876  mclsrcl  36073  mclsval  36075  nmulprop  36702  ivthALT  36886  isfne  36890  topfne  36905  neibastop3  36913  tailfb  36928  filnetlem1  36929  filnetlem4  36932  relowlssretop  38049  rdgssun  38064  poimirlem24  38335  mblfinlem2  38349  sstotbnd2  38465  sstotbnd  38466  sstotbnd3  38467  ssbnd  38479  cntotbnd  38487  cnpwstotbnd  38488  ismtyres  38499  heibor1lem  38500  heiborlem1  38502  heiborlem6  38507  heiborlem8  38509  exidreslem  38568  scottexf  38857  scott0f  38858  cnvref4  39039  dfrefrels2  39282  dfrefrel2  39284  lshpcmp  39802  lsmsat  39822  lsmsatcv  39824  lfl1dim  39935  lfl1dim2N  39936  lkrss2N  39983  psubspset  40558  paddss  40659  psubclsetN  40750  dilfsetN  40966  dilsetN  40967  diaglbN  41869  dibglbN  41980  dihlspsnat  42147  dihglb2  42156  dochffval  42163  dochfval  42164  dochvalr  42171  dochord2N  42185  dochsncom  42196  dihjat1lem  42242  dvh4dimat  42252  dvh3dimatN  42253  dvh2dimatN  42254  dochexmidlem1  42274  lpolsetN  42296  lpolconN  42301  hdmaplkr  42727  hdmapoc  42745  hlhillcs  42772  ismrc  43472  incssnn0  43482  nacsfix  43483  hbt  43897  oacl2g  44097  omcl2  44100  ofoaf  44122  naddwordnexlem4  44168  ss2iundf  44425  clsk1indlem1  44811  clsk1independent  44812  isotone1  44814  isotone2  44815  ntrclsiso  44833  ntrclsk2  44834  ssinc  45845  uzfissfz  46082  stoweidlem50  46804  stoweidlem57  46811  fourierdlem20  46881  fourierdlem50  46910  fourierdlem64  46924  fourierdlem86  46946  fourierdlem103  46963  fourierdlem104  46964  ovnval  47295  hoicvrrex  47310  ovnlecvr  47312  ovncvrrp  47318  ovnsubaddlem1  47324  hoidmvlelem3  47351  hoidmvle  47354  ovnhoilem1  47355  ovnhoi  47357  ovnlecvr2  47364  ovncvr2  47365  hspmbl  47383  ovolval4lem2  47404  ovolval5lem2  47407  ovolval5lem3  47408  ovolval5  47409  ovnovollem1  47410  ovnovollem2  47411  sprsymrelfvlem  48279  grlimedgclnbgr  48800  grlimgrtri  48808  grilcbri2  48816  uspgrsprf  48951  uspgrsprfo  48953  ssnn0ssfz  49169  lincfsuppcl  49233  iunlub  49639  lubeldm2d  49776  glbeldm2d  49777