Theorem sseq1d 3981

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq1d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq1 3975	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  sseq12d  3983  eqsstrd  3984  ssiun2s  5015  disjxiun  5107  treq  5225  iunopeqop  5484  dfpo2  6272  preddowncl  6308  funimass1  6601  f1imadifssran  6605  feq1  6669  focofo  6788  fvmptss  6983  fvimacnvi  7027  fvimacnvALT  7032  knatar  7335  ovmptss  8075  fnsuppres  8173  frecseq123  8264  csbfrecsg  8266  frrlem1  8268  frrlem3  8270  frrlem4  8271  frrlem13  8280  frrdmcl  8290  fprresex  8292  dfrecs3  8344  oaordi  8513  oaword2  8520  oawordeulem  8521  omword1  8540  oewordri  8559  oeordsuc  8561  nnaordi  8585  nnawordex  8604  naddcllem  8643  naddunif  8660  ereq1  8681  elpm2r  8821  inficl  9383  fipwss  9387  dffi3  9389  hartogslem1  9502  inf3lema  9584  inf3lemd  9587  cantnfle  9631  cantnflem2  9650  ttrclselem1  9685  trcl  9688  tcmin  9701  rankr1ai  9758  rankxplim  9839  scottex  9845  scott0  9846  scottexs  9847  scott0s  9848  karden  9855  cardne  9925  cardaleph  10049  ackbij2  10202  cflim2  10223  cfslb  10226  coftr  10233  fin23lem15  10294  fin23lem32  10304  fin23lem34  10306  fin23lem35  10307  fin23lem36  10308  fin23lem41  10312  isf32lem1  10313  itunitc1  10380  axdc3lem2  10411  ttukeylem1  10469  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwe2lem4  10594  fpwwe2  10603  fpwwecbv  10604  fpwwelem  10605  canthwelem  10610  canthwe  10611  pwfseqlem4  10622  wunex2  10698  wuncval2  10707  eltsk2g  10711  tskpwss  10712  inar1  10735  grothpw  10786  grothpwex  10787  axgroth6  10788  grothac  10790  peano5uzti  12631  fsuppmapnn0fiub0  13965  relexpnndm  15014  rtrclreclem4  15034  dfrtrcl2  15035  lo1o1  15505  o1lo1  15510  o1lo12  15511  lo1eq  15541  rlimeq  15542  isercoll  15641  prmreclem4  16897  vdwmc  16956  vdwlem1  16959  vdwlem2  16960  vdwlem12  16970  vdwlem13  16971  ramval  16986  ramz2  17002  ramub1lem1  17004  isacs2  17621  isacs1i  17625  mreacs  17626  acsfn  17627  rescabs  17802  ipole  18500  ipodrsima  18507  isacs5  18514  symgsssg  19404  psgnunilem5  19431  sylow1  19540  efgval2  19661  efgsfo  19676  frgpuplem  19709  gsumzf1o  19849  gsumzoppg  19881  dprdcntz  19947  islbs2  21071  frlmssuvc1  21710  frlmssuvc2  21711  frlmsslsp  21712  ismhp  22034  pptbas  22902  pnfnei  23114  mnfnei  23115  iscnp  23131  iscnp4  23157  cnntr  23169  cnconst2  23177  cnpresti  23182  cnprest  23183  isreg  23226  isnrm  23229  isnrm2  23252  perfcls  23259  isreg2  23271  hauscmplem  23300  1stcfb  23339  1stcelcls  23355  1stccnp  23356  txbas  23461  ptbasfi  23475  xkoopn  23483  xkoccn  23513  txcnp  23514  ptcnplem  23515  txdis  23526  txdis1cn  23529  txtube  23534  txkgen  23546  xkohaus  23547  xkoptsub  23548  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  xkococn  23554  xkoinjcn  23581  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  reghmph  23687  nrmhmph  23688  trfil2  23781  ufileu  23813  elfm  23841  elfm2  23842  elfm3  23844  imaelfm  23845  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem4  23851  fmco  23855  elflim2  23858  flffbas  23889  lmflf  23899  txflf  23900  fclscf  23919  flimfnfcls  23922  cnextcn  23961  symgtgp  24000  ghmcnp  24009  qustgplem  24015  eltsms  24027  ustval  24097  ust0  24114  trust  24124  utoptop  24129  restutop  24132  restutopopn  24133  utopsnneiplem  24142  ucncn  24179  fmucnd  24186  cfilufg  24187  trcfilu  24188  neipcfilu  24190  blssps  24319  blss  24320  ssblex  24323  blin2  24324  metss2  24407  metrest  24419  metcnp3  24435  metustexhalf  24451  metustbl  24461  psmetutop  24462  xrsmopn  24708  recld2  24710  icccmplem1  24718  icccmplem2  24719  icccmp  24721  reconnlem2  24723  lebnumlem3  24869  lebnum  24870  xlebnum  24871  lebnumii  24872  nmhmcn  25027  cfilfval  25171  caubl  25215  caublcls  25216  bcthlem1  25231  bcth  25236  ovolfiniun  25409  ovoliunlem3  25412  ovoliun  25413  ovoliun2  25414  ovoliunnul  25415  voliunlem3  25460  dyadmax  25506  dyadmbllem  25507  dyadmbl  25508  opnmbllem  25509  ellimc2  25785  limcnlp  25786  ellimc3  25787  limcflf  25789  limciun  25802  cpnord  25844  lhop  25928  xrlimcnp  26885  cvxcl  26902  dchrval  27152  noetalem2  27661  madebdayim  27806  madebdaylemold  27816  madebday  27818  precsexlem8  28123  ausgrumgri  29101  ausgrusgri  29102  nbgrval  29270  nbgrel  29274  nbumgrvtx  29280  nbgrnself  29293  uvtxel1  29330  wlkonl1iedg  29600  crctcshwlkn0lem6  29752  2wlkdlem10  29872  1wlkdlem4  30076  3wlkdlem6  30101  3wlkdlem10  30105  eupth2lem3lem4  30167  frcond1  30202  frgr1v  30207  nfrgr2v  30208  frgr3vlem1  30209  frgr3vlem2  30210  frgr3v  30211  4cycl2vnunb  30226  n4cyclfrgr  30227  isssp  30660  ubthlem1  30806  shmodi  31326  chsupid  31348  chsscon3  31436  spansncvi  31588  mdslmd1lem3  32263  mdslmd1lem4  32264  mdsymlem5  32343  dmdbr5ati  32358  dmdbr6ati  32359  dmdbr7ati  32360  ssiun2sf  32495  fpwrelmapffslem  32662  prodindf  32793  pwrssmgc  32933  fldgenval  33269  unitprodclb  33367  resssra  33590  constrsscn  33737  constrextdg2lem  33745  constrextdg2  33746  txomap  33831  locfinreflem  33837  tpr2rico  33909  pnfneige0  33948  rrhre  34018  dya2icoseg2  34276  omsfval  34292  eulerpartlemt0  34367  eulerpartgbij  34370  eulerpartlemr  34372  eulerpartlemgs2  34378  eulerpartlemn  34379  eulerpart  34380  bnj517  34882  bnj1014  34958  bnj1015  34959  bnj1123  34983  bnj1125  34989  bnj1450  35047  bnj1452  35049  cplgredgex  35115  kur14  35210  cvmliftlem15  35292  cvmlift2lem12  35308  cvmlift2lem13  35309  mclsval  35557  mclsax  35563  mclsppslem  35577  prodeq12sdv  36213  cbvsumdavw2  36290  cbvproddavw2  36291  opnrebl  36315  opnrebl2  36316  ivthALT  36330  neibastop2lem  36355  fnemeet1  36361  filnetlem1  36373  filnetlem4  36376  bj-imdirval3  37179  bj-imdiridlem  37180  rdgssun  37373  lindsadd  37614  lindsenlbs  37616  ptrecube  37621  poimirlem32  37653  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  mblfinlem3  37660  ovoliunnfl  37663  ex-ovoliunnfl  37664  voliunnfl  37665  totbndbnd  37790  heibor1lem  37810  heiborlem10  37821  scottexf  38169  scott0f  38170  relcnveq2  38318  cnvref4  38339  elrelscnveq2  38491  dfcnvrefrels2  38526  dfcnvrefrel2  38528  symrefref2  38561  lcv1  39041  lfl1dim  39121  lfl1dim2N  39122  paddasslem17  39837  dihglblem6  41341  dochvalr  41358  dochord3  41373  lpolconN  41488  lcfls1lem  41535  mapdffval  41627  mapdfval  41628  mapdsn2  41643  mapd0  41666  lspindp5  41771  mapdh8ab  41778  primrootscoprbij  42097  aks6d1c2  42125  aks6d1c6lem3  42167  aks6d1c6lem5  42172  aks6d1c7lem1  42175  ismrcd1  42693  nacsfix  42707  setindtr  43020  hbtlem6  43125  oaabsb  43290  tfsconcatrnss  43346  naddwordnexlem4  43397  clcnvlem  43619  iunrelexpmin1  43704  iunrelexpmin2  43708  relexp0a  43712  cotrcltrcl  43721  trclimalb2  43722  cotrclrcl  43738  sbcheg  43775  clsk1indlem1  44041  isotone1  44044  isotone2  44045  ntrclsiso  44063  ntrclsk2  44064  k0004lem1  44143  k0004lem3  44145  scottelrankd  44243  mnuop123d  44258  mnuprdlem1  44268  mnuprdlem2  44269  mnuunid  44273  mnurndlem1  44277  modelaxreplem1  44975  modelaxreplem2  44976  modelaxrep  44978  ssdec  45089  iinssd  45132  iinssdf  45140  ssnnf1octb  45195  iooiinicc  45547  iooiinioc  45561  icccncfext  45892  fourierdlem41  46153  meaiininclem  46491  hoidmvlelem3  46602  hoidmvle  46605  opnvonmbllem1  46637  opnvonmbl  46639  iinhoiicclem  46678  smflim  46782  smflimsuplem7  46831  clnbgrval  47827  clnbgrel  47833  sclnbgrel  47851  isubgredg  47870  isubgruhgr  47872  uhgrimisgrgriclem  47934  uhgrimisgrgric  47935  clnbgrgrimlem  47937  clnbgrgrim  47938  isubgr3stgrlem7  47975  uspgrlimlem1  47991  uspgrlimlem2  47992  uspgrlimlem3  47993  uspgrlim  47995  pgnbgreunbgr  48119  uspgrsprf  48138  iinglb  48814  iscnrm3r  48940  iscnrm3l  48943  imassc  49146  setrecseq  49678  setrec1lem4  49683  setrec2fun  49685