Theorem sseq2d 3963

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

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

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 2155  ax-ext 2733

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

This theorem is used by:  sseq12d  3964  sseqtrd  3967  sbcrel  5757  funimass2  6615  fnssresb  6653  fnimaeq0  6664  foimacnv  6834  fvelimab  6949  ssimaexg  6963  ralima  7235  knatar  7359  frecseq123  8284  frrlem4  8291  onfununi  8333  oaordi  8538  oawordeulem  8546  oaass  8553  odi  8571  omass  8572  oen0  8579  oelim2  8588  nnaordi  8611  nnawordex  8630  naddunif  8687  pssnn  9168  fissuni  9330  dffi3  9407  cantnfle  9656  cantnflem1  9674  trcl  9713  r1sdom  9764  scottex  9914  scottelrankd  9929  iscard2  10038  alephordi  10134  alephgeom  10142  cardaleph  10149  cardalephex  10150  ackbij2lem4  10300  cflm  10308  cfslbn  10326  cofsmo  10328  cfsmolem  10329  cfcoflem  10331  coftr  10332  alephsing  10335  fin23lem28  10399  fin23lem30  10401  fin23lem33  10404  fin1a2lem9  10467  axdc3lem2  10510  ttukeylem5  10572  pwfseqlem4a  10727  pwfseqlem4  10728  wunex2  10804  inar1  10841  sstskm  10908  fsuppmapnn0fiubex  14115  swrdnd  14784  swrd0  14788  repswswrd  14915  rtrclreclem1  15190  rtrclreclem2  15192  summolem2  15862  summo  15863  zsum  15864  sumz  15868  sumss  15870  fsumcvg3  15875  prodmolem2  16082  prodmo  16083  zprod  16084  prod1  16091  vdwlem1  17139  vdwlem12  17150  vdwlem13  17151  ramub2  17172  rami  17173  ramz2  17182  setsstruct2  17332  prdsval  17606  pwsle  17644  mrcuni  17775  gsumpropd  18847  gsumpropd2lem  18848  gsumress  18851  eqgfval  19368  sscntz  19520  resscntz  19527  lsmlub  19858  efgrelexlemb  19944  efgcpbllemb  19949  gsumval3a  20097  gsumzaddlem  20115  gsumzoppg  20138  dmdprd  20194  dprdcntz  20204  subgdmdprd  20230  subrngpropd  20800  subrgpropd  20840  islss  21189  lsslss  21216  lsspropd  21272  lsmelpr  21346  lbspropd  21354  lsslinds  22117  ltbval  22332  opsrval  22335  mhpval  22440  isbasisg  23245  tgval  23253  tgss3  23284  restbas  23456  tgrest  23457  restcld  23470  restopn2  23475  restntr  23480  cnpnei  23562  cncls2  23571  perfcls  23663  cmpsublem  23697  cmpsub  23698  cmpcld  23700  uncmp  23701  hauscmplem  23704  cmpfi  23706  nconnsubb  23721  clsconn  23728  hausllycmp  23793  1stckgenlem  23852  txbas  23866  ptbasfi  23880  txcnpi  23907  ptcnp  23921  txcmplem1  23940  txcmplem2  23941  xkococnlem  23958  qtopcld  24012  fbasssin  24135  fbssint  24137  fbun  24139  fbasrn  24183  filufint  24219  ufinffr  24228  ufildr  24230  ustval  24502  trust  24528  elmopn  24741  neibl  24800  cfilucfil  24858  icccmplem1  25122  icccmplem2  25123  bndth  25259  isphtpc  25295  metcld  25607  bcthlem1  25625  bcth  25630  ovolfioo  25768  ovolficc  25769  elovolmr  25777  ovoliunlem3  25805  ovolicc2  25823  volsuplem  25856  dyadmax  25899  dyadmbllem  25900  dyadmbl  25901  precsexlem6  28580  precsexlem7  28581  bdayfinbndlem1  28835  bdayfinbndlem2  28836  lnssplng  29252  incistruhgr  29639  edgssv2  29761  wksfval  30172  subgrwlk  30251  2wlkdlem9  30505  3wlkdlem9  30751  sspval  31307  ubth  31457  orthin  32030  chssoc  32080  chsscon3  32084  chsscon1  32085  h1datom  32166  pjoml6i  32173  osum  32229  spansncv  32237  pjcjt2  32276  pjopyth  32304  hstel2  32803  hstle  32814  stj  32819  dmdbr5  32892  mdslmd1lem1  32909  atord  32972  chirredlem4  32977  atcvat4i  32981  mdsymlem2  32988  mdsymlem3  32989  mdsymlem8  32994  padct  33292  ssnnssfz  33361  pwrssmgc  33543  lindspropd  33920  idlsrgval  34017  constr01  34356  constrmon  34358  constrextdg2lem  34362  constrextdg2  34363  constrfiss  34365  tpr2rico  34526  ordtrestNEW  34535  sigaval  34725  issiga  34726  issgon  34737  oms0  34912  omssubadd  34915  elscottrankss  35725  kur14  35950  cvmliftlem15  36032  satfsschain  36098  mclsrcl  36295  mclsval  36297  nmulprop  36909  ivthALT  37093  isfne  37097  topfne  37112  neibastop3  37120  tailfb  37135  filnetlem1  37136  filnetlem4  37139  relowlssretop  38254  rdgssun  38269  poimirlem24  38530  mblfinlem2  38544  sstotbnd2  38676  sstotbnd  38677  sstotbnd3  38678  ssbnd  38690  cntotbnd  38698  cnpwstotbnd  38699  ismtyres  38710  heibor1lem  38711  heiborlem1  38713  heiborlem6  38718  heiborlem8  38720  exidreslem  38779  scottexf  39068  scott0f  39069  cnvref4  39250  dfrefrels2  39493  dfrefrel2  39495  lshpcmp  40013  lsmsat  40033  lsmsatcv  40035  lfl1dim  40146  lfl1dim2N  40147  lkrss2N  40194  psubspset  40769  paddss  40870  psubclsetN  40961  dilfsetN  41177  dilsetN  41178  diaglbN  42080  dibglbN  42191  dihlspsnat  42358  dihglb2  42367  dochffval  42374  dochfval  42375  dochvalr  42382  dochord2N  42396  dochsncom  42407  dihjat1lem  42453  dvh4dimat  42463  dvh3dimatN  42464  dvh2dimatN  42465  dochexmidlem1  42485  lpolsetN  42507  lpolconN  42512  hdmaplkr  42938  hdmapoc  42956  hlhillcs  42983  ismrc  43665  incssnn0  43675  nacsfix  43676  hbt  44090  oacl2g  44290  omcl2  44293  ofoaf  44315  naddwordnexlem4  44361  ss2iundf  44618  clsk1indlem1  45004  clsk1independent  45005  isotone1  45007  isotone2  45008  ntrclsiso  45026  ntrclsk2  45027  ssinc  46045  uzfissfz  46282  stoweidlem50  47004  stoweidlem57  47011  fourierdlem20  47081  fourierdlem50  47110  fourierdlem64  47124  fourierdlem86  47146  fourierdlem103  47163  fourierdlem104  47164  ovnval  47495  hoicvrrex  47510  ovnlecvr  47512  ovncvrrp  47518  ovnsubaddlem1  47524  hoidmvlelem3  47551  hoidmvle  47554  ovnhoilem1  47555  ovnhoi  47557  ovnlecvr2  47564  ovncvr2  47565  hspmbl  47583  ovolval4lem2  47604  ovolval5lem2  47607  ovolval5lem3  47608  ovolval5  47609  ovnovollem1  47610  ovnovollem2  47611  sprsymrelfvlem  48516  grlimedgclnbgr  49037  grlimgrtri  49045  grilcbri2  49053  uspgrsprf  49188  uspgrsprfo  49190  ssnn0ssfz  49405  lincfsuppcl  49469  iunlub  49875  lubeldm2d  50010  glbeldm2d  50011