Theorem sseq2d 3966

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3901

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 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  sseq12d  3967  sseqtrd  3970  sbcrel  5730  funimass2  6575  fnssresb  6614  fnimaeq0  6625  foimacnv  6791  fvelimab  6906  ssimaexg  6920  ralima  7183  knatar  7303  frecseq123  8224  frrlem4  8231  onfununi  8273  oaordi  8473  oawordeulem  8481  oaass  8488  odi  8506  omass  8507  oen0  8514  oelim2  8523  nnaordi  8546  nnawordex  8565  naddunif  8621  pssnn  9093  fissuni  9257  dffi3  9334  cantnfle  9580  cantnflem1  9598  trcl  9637  r1sdom  9686  iscard2  9888  alephordi  9984  alephgeom  9992  cardaleph  9999  cardalephex  10000  ackbij2lem4  10151  cflm  10160  cfslbn  10177  cofsmo  10179  cfsmolem  10180  cfcoflem  10182  coftr  10183  alephsing  10186  fin23lem28  10250  fin23lem30  10252  fin23lem33  10255  fin1a2lem9  10318  axdc3lem2  10361  ttukeylem5  10423  pwfseqlem4a  10572  pwfseqlem4  10573  wunex2  10649  inar1  10686  sstskm  10753  fsuppmapnn0fiubex  13915  swrdnd  14578  swrd0  14582  repswswrd  14707  rtrclreclem1  14980  rtrclreclem2  14982  summolem2  15639  summo  15640  zsum  15641  sumz  15645  sumss  15647  fsumcvg3  15652  prodmolem2  15858  prodmo  15859  zprod  15860  prod1  15867  vdwlem1  16909  vdwlem12  16920  vdwlem13  16921  ramub2  16942  rami  16943  ramz2  16952  setsstruct2  17101  prdsval  17375  pwsle  17413  mrcuni  17544  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  eqgfval  19105  sscntz  19255  resscntz  19262  lsmlub  19593  efgrelexlemb  19679  efgcpbllemb  19684  gsumval3a  19832  gsumzaddlem  19850  gsumzoppg  19873  dmdprd  19929  dprdcntz  19939  subgdmdprd  19965  subrngpropd  20501  subrgpropd  20541  islss  20885  lsslss  20912  lsspropd  20969  lsmelpr  21043  lbspropd  21051  lsslinds  21786  ltbval  21998  opsrval  22001  mhpval  22082  isbasisg  22891  tgval  22899  tgss3  22930  restbas  23102  tgrest  23103  restcld  23116  restopn2  23121  restntr  23126  cnpnei  23208  cncls2  23217  perfcls  23309  cmpsublem  23343  cmpsub  23344  cmpcld  23346  uncmp  23347  hauscmplem  23350  cmpfi  23352  nconnsubb  23367  clsconn  23374  hausllycmp  23438  1stckgenlem  23497  txbas  23511  ptbasfi  23525  txcnpi  23552  ptcnp  23566  txcmplem1  23585  txcmplem2  23586  xkococnlem  23603  qtopcld  23657  fbasssin  23780  fbssint  23782  fbun  23784  fbasrn  23828  filufint  23864  ufinffr  23873  ufildr  23875  ustval  24147  trust  24173  elmopn  24386  neibl  24445  cfilucfil  24503  icccmplem1  24767  icccmplem2  24768  bndth  24913  isphtpc  24949  metcld  25262  bcthlem1  25280  bcth  25285  ovolfioo  25424  ovolficc  25425  elovolmr  25433  ovoliunlem3  25461  ovolicc2  25479  volsuplem  25512  dyadmax  25555  dyadmbllem  25556  dyadmbl  25557  precsexlem6  28208  precsexlem7  28209  bdayfinbndlem1  28463  bdayfinbndlem2  28464  incistruhgr  29152  edgssv2  29271  wksfval  29683  2wlkdlem9  30007  3wlkdlem9  30243  sspval  30798  ubth  30948  orthin  31521  chssoc  31571  chsscon3  31575  chsscon1  31576  h1datom  31657  pjoml6i  31664  osum  31720  spansncv  31728  pjcjt2  31767  pjopyth  31795  hstel2  32294  hstle  32305  stj  32310  dmdbr5  32383  mdslmd1lem1  32400  atord  32463  chirredlem4  32468  atcvat4i  32472  mdsymlem2  32479  mdsymlem3  32480  mdsymlem8  32485  padct  32797  ssnnssfz  32867  pwrssmgc  33082  lindspropd  33464  idlsrgval  33584  constr01  33899  constrmon  33901  constrextdg2lem  33905  constrextdg2  33906  constrfiss  33908  tpr2rico  34069  ordtrestNEW  34078  sigaval  34268  issiga  34269  issgon  34280  oms0  34454  omssubadd  34457  subgrwlk  35326  umgr2cycllem  35334  kur14  35410  cvmliftlem15  35492  satfsschain  35558  mclsrcl  35755  mclsval  35757  ivthALT  36529  isfne  36533  topfne  36548  neibastop3  36556  tailfb  36571  filnetlem1  36572  filnetlem4  36575  relowlssretop  37564  rdgssun  37579  poimirlem24  37841  mblfinlem2  37855  sstotbnd2  37971  sstotbnd  37972  sstotbnd3  37973  ssbnd  37985  cntotbnd  37993  cnpwstotbnd  37994  ismtyres  38005  heibor1lem  38006  heiborlem1  38008  heiborlem6  38013  heiborlem8  38015  exidreslem  38074  scottexf  38365  scott0f  38366  cnvref4  38539  dfrefrels2  38762  dfrefrel2  38764  lshpcmp  39244  lsmsat  39264  lsmsatcv  39266  lfl1dim  39377  lfl1dim2N  39378  lkrss2N  39425  psubspset  40000  paddss  40101  psubclsetN  40192  dilfsetN  40408  dilsetN  40409  diaglbN  41311  dibglbN  41422  dihlspsnat  41589  dihglb2  41598  dochffval  41605  dochfval  41606  dochvalr  41613  dochord2N  41627  dochsncom  41638  dihjat1lem  41684  dvh4dimat  41694  dvh3dimatN  41695  dvh2dimatN  41696  dochexmidlem1  41716  lpolsetN  41738  lpolconN  41743  hdmaplkr  42169  hdmapoc  42187  hlhillcs  42214  ismrc  42939  incssnn0  42949  nacsfix  42950  hbt  43368  oacl2g  43568  omcl2  43571  ofoaf  43593  naddwordnexlem4  43639  ss2iundf  43896  clsk1indlem1  44282  clsk1independent  44283  isotone1  44285  isotone2  44286  ntrclsiso  44304  ntrclsk2  44305  scottelrankd  44484  ssinc  45327  uzfissfz  45567  stoweidlem50  46290  stoweidlem57  46297  fourierdlem20  46367  fourierdlem50  46396  fourierdlem64  46410  fourierdlem86  46432  fourierdlem103  46449  fourierdlem104  46450  ovnval  46781  hoicvrrex  46796  ovnlecvr  46798  ovncvrrp  46804  ovnsubaddlem1  46810  hoidmvlelem3  46837  hoidmvle  46840  ovnhoilem1  46841  ovnhoi  46843  ovnlecvr2  46850  ovncvr2  46851  hspmbl  46869  ovolval4lem2  46890  ovolval5lem2  46893  ovolval5lem3  46894  ovolval5  46895  ovnovollem1  46896  ovnovollem2  46897  sprsymrelfvlem  47732  grlimedgclnbgr  48237  grlimgrtri  48245  grilcbri2  48253  uspgrsprf  48388  uspgrsprfo  48390  ssnn0ssfz  48591  lincfsuppcl  48655  iunlub  49062  lubeldm2d  49199  glbeldm2d  49200