Theorem sseq2d 3954

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  sseq12d  3955  sseqtrd  3958  sbcrel  5737  funimass2  6581  fnssresb  6620  fnimaeq0  6631  foimacnv  6797  fvelimab  6912  ssimaexg  6926  ralima  7192  knatar  7312  frecseq123  8232  frrlem4  8239  onfununi  8281  oaordi  8481  oawordeulem  8489  oaass  8496  odi  8514  omass  8515  oen0  8522  oelim2  8531  nnaordi  8554  nnawordex  8573  naddunif  8629  pssnn  9103  fissuni  9267  dffi3  9344  cantnfle  9592  cantnflem1  9610  trcl  9649  r1sdom  9698  iscard2  9900  alephordi  9996  alephgeom  10004  cardaleph  10011  cardalephex  10012  ackbij2lem4  10163  cflm  10172  cfslbn  10189  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  coftr  10195  alephsing  10198  fin23lem28  10262  fin23lem30  10264  fin23lem33  10267  fin1a2lem9  10330  axdc3lem2  10373  ttukeylem5  10435  pwfseqlem4a  10584  pwfseqlem4  10585  wunex2  10661  inar1  10698  sstskm  10765  fsuppmapnn0fiubex  13954  swrdnd  14617  swrd0  14621  repswswrd  14746  rtrclreclem1  15019  rtrclreclem2  15021  summolem2  15678  summo  15679  zsum  15680  sumz  15684  sumss  15686  fsumcvg3  15691  prodmolem2  15900  prodmo  15901  zprod  15902  prod1  15909  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  ramub2  16985  rami  16986  ramz2  16995  setsstruct2  17144  prdsval  17418  pwsle  17456  mrcuni  17587  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  eqgfval  19151  sscntz  19301  resscntz  19308  lsmlub  19639  efgrelexlemb  19725  efgcpbllemb  19730  gsumval3a  19878  gsumzaddlem  19896  gsumzoppg  19919  dmdprd  19975  dprdcntz  19985  subgdmdprd  20011  subrngpropd  20545  subrgpropd  20585  islss  20929  lsslss  20956  lsspropd  21012  lsmelpr  21086  lbspropd  21094  lsslinds  21811  ltbval  22021  opsrval  22024  mhpval  22105  isbasisg  22912  tgval  22920  tgss3  22951  restbas  23123  tgrest  23124  restcld  23137  restopn2  23142  restntr  23147  cnpnei  23229  cncls2  23238  perfcls  23330  cmpsublem  23364  cmpsub  23365  cmpcld  23367  uncmp  23368  hauscmplem  23371  cmpfi  23373  nconnsubb  23388  clsconn  23395  hausllycmp  23459  1stckgenlem  23518  txbas  23532  ptbasfi  23546  txcnpi  23573  ptcnp  23587  txcmplem1  23606  txcmplem2  23607  xkococnlem  23624  qtopcld  23678  fbasssin  23801  fbssint  23803  fbun  23805  fbasrn  23849  filufint  23885  ufinffr  23894  ufildr  23896  ustval  24168  trust  24194  elmopn  24407  neibl  24466  cfilucfil  24524  icccmplem1  24788  icccmplem2  24789  bndth  24925  isphtpc  24961  metcld  25273  bcthlem1  25291  bcth  25296  ovolfioo  25434  ovolficc  25435  elovolmr  25443  ovoliunlem3  25471  ovolicc2  25489  volsuplem  25522  dyadmax  25565  dyadmbllem  25566  dyadmbl  25567  precsexlem6  28204  precsexlem7  28205  bdayfinbndlem1  28459  bdayfinbndlem2  28460  incistruhgr  29148  edgssv2  29267  wksfval  29678  2wlkdlem9  30002  3wlkdlem9  30238  sspval  30794  ubth  30944  orthin  31517  chssoc  31567  chsscon3  31571  chsscon1  31572  h1datom  31653  pjoml6i  31660  osum  31716  spansncv  31724  pjcjt2  31763  pjopyth  31791  hstel2  32290  hstle  32301  stj  32306  dmdbr5  32379  mdslmd1lem1  32396  atord  32459  chirredlem4  32464  atcvat4i  32468  mdsymlem2  32475  mdsymlem3  32476  mdsymlem8  32481  padct  32791  ssnnssfz  32860  pwrssmgc  33060  lindspropd  33443  idlsrgval  33563  constr01  33886  constrmon  33888  constrextdg2lem  33892  constrextdg2  33893  constrfiss  33895  tpr2rico  34056  ordtrestNEW  34065  sigaval  34255  issiga  34256  issgon  34267  oms0  34441  omssubadd  34444  subgrwlk  35314  umgr2cycllem  35322  kur14  35398  cvmliftlem15  35480  satfsschain  35546  mclsrcl  35743  mclsval  35745  ivthALT  36517  isfne  36521  topfne  36536  neibastop3  36544  tailfb  36559  filnetlem1  36560  filnetlem4  36563  relowlssretop  37679  rdgssun  37694  poimirlem24  37965  mblfinlem2  37979  sstotbnd2  38095  sstotbnd  38096  sstotbnd3  38097  ssbnd  38109  cntotbnd  38117  cnpwstotbnd  38118  ismtyres  38129  heibor1lem  38130  heiborlem1  38132  heiborlem6  38137  heiborlem8  38139  exidreslem  38198  scottexf  38489  scott0f  38490  cnvref4  38671  dfrefrels2  38914  dfrefrel2  38916  lshpcmp  39434  lsmsat  39454  lsmsatcv  39456  lfl1dim  39567  lfl1dim2N  39568  lkrss2N  39615  psubspset  40190  paddss  40291  psubclsetN  40382  dilfsetN  40598  dilsetN  40599  diaglbN  41501  dibglbN  41612  dihlspsnat  41779  dihglb2  41788  dochffval  41795  dochfval  41796  dochvalr  41803  dochord2N  41817  dochsncom  41828  dihjat1lem  41874  dvh4dimat  41884  dvh3dimatN  41885  dvh2dimatN  41886  dochexmidlem1  41906  lpolsetN  41928  lpolconN  41933  hdmaplkr  42359  hdmapoc  42377  hlhillcs  42404  ismrc  43133  incssnn0  43143  nacsfix  43144  hbt  43558  oacl2g  43758  omcl2  43761  ofoaf  43783  naddwordnexlem4  43829  ss2iundf  44086  clsk1indlem1  44472  clsk1independent  44473  isotone1  44475  isotone2  44476  ntrclsiso  44494  ntrclsk2  44495  scottelrankd  44674  ssinc  45517  uzfissfz  45756  stoweidlem50  46478  stoweidlem57  46485  fourierdlem20  46555  fourierdlem50  46584  fourierdlem64  46598  fourierdlem86  46620  fourierdlem103  46637  fourierdlem104  46638  ovnval  46969  hoicvrrex  46984  ovnlecvr  46986  ovncvrrp  46992  ovnsubaddlem1  46998  hoidmvlelem3  47025  hoidmvle  47028  ovnhoilem1  47029  ovnhoi  47031  ovnlecvr2  47038  ovncvr2  47039  hspmbl  47057  ovolval4lem2  47078  ovolval5lem2  47081  ovolval5lem3  47082  ovolval5  47083  ovnovollem1  47084  ovnovollem2  47085  sprsymrelfvlem  47950  grlimedgclnbgr  48471  grlimgrtri  48479  grilcbri2  48487  uspgrsprf  48622  uspgrsprfo  48624  ssnn0ssfz  48825  lincfsuppcl  48889  iunlub  49296  lubeldm2d  49433  glbeldm2d  49434