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 207   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseq12d  3955  sseqtrd  3958  sbcrel  5731  funimass2  6575  fnssresb  6614  fnimaeq0  6625  foimacnv  6791  fvelimab  6906  ssimaexg  6920  ralima  7188  knatar  7308  frecseq123  8229  frrlem4  8236  onfununi  8278  oaordi  8478  oawordeulem  8486  oaass  8493  odi  8511  omass  8512  oen0  8519  oelim2  8528  nnaordi  8551  nnawordex  8570  naddunif  8626  pssnn  9100  fissuni  9264  dffi3  9341  cantnfle  9590  cantnflem1  9608  trcl  9647  r1sdom  9696  iscard2  9898  alephordi  9994  alephgeom  10002  cardaleph  10009  cardalephex  10010  ackbij2lem4  10161  cflm  10170  cfslbn  10187  cofsmo  10189  cfsmolem  10190  cfcoflem  10192  coftr  10193  alephsing  10196  fin23lem28  10260  fin23lem30  10262  fin23lem33  10265  fin1a2lem9  10328  axdc3lem2  10371  ttukeylem5  10433  pwfseqlem4a  10582  pwfseqlem4  10583  wunex2  10659  inar1  10696  sstskm  10763  fsuppmapnn0fiubex  13952  swrdnd  14615  swrd0  14619  repswswrd  14744  rtrclreclem1  15017  rtrclreclem2  15019  summolem2  15676  summo  15677  zsum  15678  sumz  15682  sumss  15684  fsumcvg3  15689  prodmolem2  15898  prodmo  15899  zprod  15900  prod1  15907  vdwlem1  16950  vdwlem12  16961  vdwlem13  16962  ramub2  16983  rami  16984  ramz2  16993  setsstruct2  17142  prdsval  17416  pwsle  17454  mrcuni  17585  gsumpropd  18644  gsumpropd2lem  18645  gsumress  18648  eqgfval  19149  sscntz  19299  resscntz  19306  lsmlub  19637  efgrelexlemb  19723  efgcpbllemb  19728  gsumval3a  19876  gsumzaddlem  19894  gsumzoppg  19917  dmdprd  19973  dprdcntz  19983  subgdmdprd  20009  subrngpropd  20547  subrgpropd  20587  islss  20931  lsslss  20958  lsspropd  21014  lsmelpr  21088  lbspropd  21096  lsslinds  21813  ltbval  22026  opsrval  22029  mhpval  22134  isbasisg  22937  tgval  22945  tgss3  22976  restbas  23148  tgrest  23149  restcld  23162  restopn2  23167  restntr  23172  cnpnei  23254  cncls2  23263  perfcls  23355  cmpsublem  23389  cmpsub  23390  cmpcld  23392  uncmp  23393  hauscmplem  23396  cmpfi  23398  nconnsubb  23413  clsconn  23420  hausllycmp  23484  1stckgenlem  23543  txbas  23557  ptbasfi  23571  txcnpi  23598  ptcnp  23612  txcmplem1  23631  txcmplem2  23632  xkococnlem  23649  qtopcld  23703  fbasssin  23826  fbssint  23828  fbun  23830  fbasrn  23874  filufint  23910  ufinffr  23919  ufildr  23921  ustval  24193  trust  24219  elmopn  24432  neibl  24491  cfilucfil  24549  icccmplem1  24813  icccmplem2  24814  bndth  24950  isphtpc  24986  metcld  25298  bcthlem1  25316  bcth  25321  ovolfioo  25459  ovolficc  25460  elovolmr  25468  ovoliunlem3  25496  ovolicc2  25514  volsuplem  25547  dyadmax  25590  dyadmbllem  25591  dyadmbl  25592  precsexlem6  28229  precsexlem7  28230  bdayfinbndlem1  28484  bdayfinbndlem2  28485  incistruhgr  29173  edgssv2  29292  wksfval  29703  2wlkdlem9  30027  3wlkdlem9  30263  sspval  30819  ubth  30969  orthin  31542  chssoc  31592  chsscon3  31596  chsscon1  31597  h1datom  31678  pjoml6i  31685  osum  31741  spansncv  31749  pjcjt2  31788  pjopyth  31816  hstel2  32315  hstle  32326  stj  32331  dmdbr5  32404  mdslmd1lem1  32421  atord  32484  chirredlem4  32489  atcvat4i  32493  mdsymlem2  32500  mdsymlem3  32501  mdsymlem8  32506  padct  32817  ssnnssfz  32886  pwrssmgc  33086  lindspropd  33473  idlsrgval  33593  constr01  33933  constrmon  33935  constrextdg2lem  33939  constrextdg2  33940  constrfiss  33942  tpr2rico  34103  ordtrestNEW  34112  sigaval  34302  issiga  34303  issgon  34314  oms0  34488  omssubadd  34491  subgrwlk  35367  umgr2cycllem  35375  kur14  35451  cvmliftlem15  35533  satfsschain  35599  mclsrcl  35796  mclsval  35798  ivthALT  36570  isfne  36574  topfne  36589  neibastop3  36597  tailfb  36612  filnetlem1  36613  filnetlem4  36616  relowlssretop  37732  rdgssun  37747  poimirlem24  38018  mblfinlem2  38032  sstotbnd2  38148  sstotbnd  38149  sstotbnd3  38150  ssbnd  38162  cntotbnd  38170  cnpwstotbnd  38171  ismtyres  38182  heibor1lem  38183  heiborlem1  38185  heiborlem6  38190  heiborlem8  38192  exidreslem  38251  scottexf  38542  scott0f  38543  cnvref4  38724  dfrefrels2  38967  dfrefrel2  38969  lshpcmp  39487  lsmsat  39507  lsmsatcv  39509  lfl1dim  39620  lfl1dim2N  39621  lkrss2N  39668  psubspset  40243  paddss  40344  psubclsetN  40435  dilfsetN  40651  dilsetN  40652  diaglbN  41554  dibglbN  41665  dihlspsnat  41832  dihglb2  41841  dochffval  41848  dochfval  41849  dochvalr  41856  dochord2N  41870  dochsncom  41881  dihjat1lem  41927  dvh4dimat  41937  dvh3dimatN  41938  dvh2dimatN  41939  dochexmidlem1  41959  lpolsetN  41981  lpolconN  41986  hdmaplkr  42412  hdmapoc  42430  hlhillcs  42457  ismrc  43157  incssnn0  43167  nacsfix  43168  hbt  43582  oacl2g  43782  omcl2  43785  ofoaf  43807  naddwordnexlem4  43853  ss2iundf  44110  clsk1indlem1  44496  clsk1independent  44497  isotone1  44499  isotone2  44500  ntrclsiso  44518  ntrclsk2  44519  scottelrankd  44698  ssinc  45541  uzfissfz  45778  stoweidlem50  46500  stoweidlem57  46507  fourierdlem20  46577  fourierdlem50  46606  fourierdlem64  46620  fourierdlem86  46642  fourierdlem103  46659  fourierdlem104  46660  ovnval  46991  hoicvrrex  47006  ovnlecvr  47008  ovncvrrp  47014  ovnsubaddlem1  47020  hoidmvlelem3  47047  hoidmvle  47050  ovnhoilem1  47051  ovnhoi  47053  ovnlecvr2  47060  ovncvr2  47061  hspmbl  47079  ovolval4lem2  47100  ovolval5lem2  47103  ovolval5lem3  47104  ovolval5  47105  ovnovollem1  47106  ovnovollem2  47107  sprsymrelfvlem  47972  grlimedgclnbgr  48493  grlimgrtri  48501  grilcbri2  48509  uspgrsprf  48644  uspgrsprfo  48646  ssnn0ssfz  48847  lincfsuppcl  48911  iunlub  49318  lubeldm2d  49455  glbeldm2d  49456