Theorem sseq2d 3940

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseq12d  3941  sseqtrd  3944  sbcrel  5756  funimass2  6623  fnssresb  6661  fnimaeq0  6672  foimacnv  6842  fvelimab  6957  ssimaexg  6971  ralima  7243  knatar  7367  frecseq123  8301  frrlem4  8308  onfununi  8350  oaordi  8555  oawordeulem  8563  oaass  8570  odi  8588  omass  8589  oen0  8596  oelim2  8605  nnaordi  8628  nnawordex  8647  naddunif  8704  pssnn  9185  fissuni  9347  dffi3  9424  cantnfle  9673  cantnflem1  9691  trcl  9730  r1sdom  9782  scottex  9934  scottelrankd  9949  iscard2  10058  alephordi  10154  alephgeom  10162  cardaleph  10169  cardalephex  10170  ackbij2lem4  10320  cflm  10328  cfslbn  10346  cofsmo  10348  cfsmolem  10349  cfcoflem  10351  coftr  10352  alephsing  10355  fin23lem28  10419  fin23lem30  10421  fin23lem33  10424  fin1a2lem9  10487  axdc3lem2  10530  ttukeylem5  10592  pwfseqlem4a  10747  pwfseqlem4  10748  wunex2  10824  inar1  10861  sstskm  10928  fsuppmapnn0fiubex  14136  swrdnd  14805  swrd0  14809  repswswrd  14936  rtrclreclem1  15211  rtrclreclem2  15213  summolem2  15883  summo  15884  zsum  15885  sumz  15889  sumss  15891  fsumcvg3  15896  prodmolem2  16103  prodmo  16104  zprod  16105  prod1  16112  vdwlem1  17160  vdwlem12  17171  vdwlem13  17172  ramub2  17193  rami  17194  ramz2  17203  setsstruct2  17353  prdsval  17627  pwsle  17665  mrcuni  17796  gsumpropd  18868  gsumpropd2lem  18869  gsumress  18872  eqgfval  19389  sscntz  19541  resscntz  19548  lsmlub  19879  efgrelexlemb  19965  efgcpbllemb  19970  gsumval3a  20118  gsumzaddlem  20136  gsumzoppg  20159  dmdprd  20215  dprdcntz  20225  subgdmdprd  20251  subrngpropd  20821  subrgpropd  20861  islss  21210  lsslss  21237  lsspropd  21293  lsmelpr  21367  lbspropd  21375  lsslinds  22138  ltbval  22353  opsrval  22356  mhpval  22461  isbasisg  23266  tgval  23274  tgss3  23305  restbas  23477  tgrest  23478  restcld  23491  restopn2  23496  restntr  23501  cnpnei  23583  cncls2  23592  perfcls  23684  cmpsublem  23718  cmpsub  23719  cmpcld  23721  uncmp  23722  hauscmplem  23725  cmpfi  23727  nconnsubb  23742  clsconn  23749  hausllycmp  23814  1stckgenlem  23873  txbas  23887  ptbasfi  23901  txcnpi  23928  ptcnp  23942  txcmplem1  23961  txcmplem2  23962  xkococnlem  23979  qtopcld  24033  fbasssin  24156  fbssint  24158  fbun  24160  fbasrn  24204  filufint  24240  ufinffr  24249  ufildr  24251  ustval  24523  trust  24549  elmopn  24762  neibl  24821  cfilucfil  24879  icccmplem1  25143  icccmplem2  25144  bndth  25280  isphtpc  25316  metcld  25628  bcthlem1  25646  bcth  25651  ovolfioo  25789  ovolficc  25790  elovolmr  25798  ovoliunlem3  25826  ovolicc2  25844  volsuplem  25877  dyadmax  25920  dyadmbllem  25921  dyadmbl  25922  precsexlem6  28599  precsexlem7  28600  bdayfinbndlem1  28854  bdayfinbndlem2  28855  lnssplng  29271  incistruhgr  29658  edgssv2  29780  wksfval  30191  subgrwlk  30270  2wlkdlem9  30524  3wlkdlem9  30770  sspval  31326  ubth  31476  orthin  32049  chssoc  32099  chsscon3  32103  chsscon1  32104  h1datom  32185  pjoml6i  32192  osum  32248  spansncv  32256  pjcjt2  32295  pjopyth  32323  hstel2  32822  hstle  32833  stj  32838  dmdbr5  32911  mdslmd1lem1  32928  atord  32991  chirredlem4  32996  atcvat4i  33000  mdsymlem2  33007  mdsymlem3  33008  mdsymlem8  33013  padct  33353  ssnnssfz  33422  pwrssmgc  33604  lindspropd  33981  idlsrgval  34078  constr01  34417  constrmon  34419  constrextdg2lem  34423  constrextdg2  34424  constrfiss  34426  tpr2rico  34587  ordtrestNEW  34596  sigaval  34786  issiga  34787  issgon  34798  oms0  34972  omssubadd  34975  elscottrankss  35794  acwer1prclem  35808  maxssj0  35938  onprcf1acwevdlem1  35957  kur14  36050  cvmliftlem15  36132  satfsschain  36198  mclsrcl  36395  mclsval  36397  nmulprop  37014  ivthALT  37198  isfne  37202  topfne  37217  neibastop3  37225  tailfb  37240  filnetlem1  37241  filnetlem4  37244  relowlssretop  38362  rdgssun  38377  poimirlem24  38638  mblfinlem2  38652  sstotbnd2  38784  sstotbnd  38785  sstotbnd3  38786  ssbnd  38798  cntotbnd  38806  cnpwstotbnd  38807  ismtyres  38818  heibor1lem  38819  heiborlem1  38821  heiborlem6  38826  heiborlem8  38828  exidreslem  38887  scottexf  39176  scott0f  39177  cnvref4  39358  dfrefrels2  39601  dfrefrel2  39603  lshpcmp  40121  lsmsat  40141  lsmsatcv  40143  lfl1dim  40254  lfl1dim2N  40255  lkrss2N  40302  psubspset  40877  paddss  40978  psubclsetN  41069  dilfsetN  41285  dilsetN  41286  diaglbN  42188  dibglbN  42299  dihlspsnat  42466  dihglb2  42475  dochffval  42482  dochfval  42483  dochvalr  42490  dochord2N  42504  dochsncom  42515  dihjat1lem  42561  dvh4dimat  42571  dvh3dimatN  42572  dvh2dimatN  42573  dochexmidlem1  42593  lpolsetN  42615  lpolconN  42620  hdmaplkr  43046  hdmapoc  43064  hlhillcs  43091  ismrc  43788  incssnn0  43798  nacsfix  43799  hbt  44208  oacl2g  44408  omcl2  44411  ofoaf  44433  naddwordnexlem4  44479  ss2iundf  44735  clsk1indlem1  45121  clsk1independent  45122  isotone1  45124  isotone2  45125  ntrclsiso  45143  ntrclsk2  45144  ssinc  46178  uzfissfz  46414  stoweidlem50  47136  stoweidlem57  47143  fourierdlem20  47213  fourierdlem50  47242  fourierdlem64  47256  fourierdlem86  47278  fourierdlem103  47295  fourierdlem104  47296  ovnval  47627  hoicvrrex  47642  ovnlecvr  47644  ovncvrrp  47650  ovnsubaddlem1  47656  hoidmvlelem3  47683  hoidmvle  47686  ovnhoilem1  47687  ovnhoi  47689  ovnlecvr2  47696  ovncvr2  47697  hspmbl  47715  ovolval4lem2  47736  ovolval5lem2  47739  ovolval5lem3  47740  ovolval5  47741  ovnovollem1  47742  ovnovollem2  47743  sprsymrelfvlem  48648  grlimedgclnbgr  49169  grlimgrtri  49177  grilcbri2  49185  uspgrsprf  49320  uspgrsprfo  49322  ssnn0ssfz  49537  lincfsuppcl  49601  iunlub  50007  lubeldm2d  50142  glbeldm2d  50143