Theorem sseq1d 3969

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

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

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 2701

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

This theorem is referenced by:  sseq12d  3971  eqsstrd  3972  ssiun2s  5000  disjxiun  5092  treq  5209  iunopeqop  5468  dfpo2  6248  preddowncl  6284  funimass1  6568  f1imadifssran  6572  feq1  6634  focofo  6753  fvmptss  6946  fvimacnvi  6990  fvimacnvALT  6995  knatar  7298  ovmptss  8033  fnsuppres  8131  frecseq123  8222  csbfrecsg  8224  frrlem1  8226  frrlem3  8228  frrlem4  8229  frrlem13  8238  frrdmcl  8248  fprresex  8250  dfrecs3  8302  oaordi  8471  oaword2  8478  oawordeulem  8479  omword1  8498  oewordri  8517  oeordsuc  8519  nnaordi  8543  nnawordex  8562  naddcllem  8601  naddunif  8618  ereq1  8639  elpm2r  8779  inficl  9334  fipwss  9338  dffi3  9340  hartogslem1  9453  inf3lema  9539  inf3lemd  9542  cantnfle  9586  cantnflem2  9605  ttrclselem1  9640  trcl  9643  tcmin  9656  rankr1ai  9713  rankxplim  9794  scottex  9800  scott0  9801  scottexs  9802  scott0s  9803  karden  9810  cardne  9880  cardaleph  10002  ackbij2  10155  cflim2  10176  cfslb  10179  coftr  10186  fin23lem15  10247  fin23lem32  10257  fin23lem34  10259  fin23lem35  10260  fin23lem36  10261  fin23lem41  10265  isf32lem1  10266  itunitc1  10333  axdc3lem2  10364  ttukeylem1  10422  fpwwe2cbv  10543  fpwwe2lem2  10545  fpwwe2lem4  10547  fpwwe2  10556  fpwwecbv  10557  fpwwelem  10558  canthwelem  10563  canthwe  10564  pwfseqlem4  10575  wunex2  10651  wuncval2  10660  eltsk2g  10664  tskpwss  10665  inar1  10688  grothpw  10739  grothpwex  10740  axgroth6  10741  grothac  10743  peano5uzti  12584  fsuppmapnn0fiub0  13918  relexpnndm  14966  rtrclreclem4  14986  dfrtrcl2  14987  lo1o1  15457  o1lo1  15462  o1lo12  15463  lo1eq  15493  rlimeq  15494  isercoll  15593  prmreclem4  16849  vdwmc  16908  vdwlem1  16911  vdwlem2  16912  vdwlem12  16922  vdwlem13  16923  ramval  16938  ramz2  16954  ramub1lem1  16956  isacs2  17577  isacs1i  17581  mreacs  17582  acsfn  17583  rescabs  17758  ipole  18458  ipodrsima  18465  isacs5  18472  symgsssg  19364  psgnunilem5  19391  sylow1  19500  efgval2  19621  efgsfo  19636  frgpuplem  19669  gsumzf1o  19809  gsumzoppg  19841  dprdcntz  19907  islbs2  21079  frlmssuvc1  21719  frlmssuvc2  21720  frlmsslsp  21721  ismhp  22043  pptbas  22911  pnfnei  23123  mnfnei  23124  iscnp  23140  iscnp4  23166  cnntr  23178  cnconst2  23186  cnpresti  23191  cnprest  23192  isreg  23235  isnrm  23238  isnrm2  23261  perfcls  23268  isreg2  23280  hauscmplem  23309  1stcfb  23348  1stcelcls  23364  1stccnp  23365  txbas  23470  ptbasfi  23484  xkoopn  23492  xkoccn  23522  txcnp  23523  ptcnplem  23524  txdis  23535  txdis1cn  23538  txtube  23543  txkgen  23555  xkohaus  23556  xkoptsub  23557  xkoco1cn  23560  xkoco2cn  23561  xkococnlem  23562  xkococn  23563  xkoinjcn  23590  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  reghmph  23696  nrmhmph  23697  trfil2  23790  ufileu  23822  elfm  23850  elfm2  23851  elfm3  23853  imaelfm  23854  rnelfm  23856  fmfnfmlem2  23858  fmfnfmlem4  23860  fmco  23864  elflim2  23867  flffbas  23898  lmflf  23908  txflf  23909  fclscf  23928  flimfnfcls  23931  cnextcn  23970  symgtgp  24009  ghmcnp  24018  qustgplem  24024  eltsms  24036  ustval  24106  ust0  24123  trust  24133  utoptop  24138  restutop  24141  restutopopn  24142  utopsnneiplem  24151  ucncn  24188  fmucnd  24195  cfilufg  24196  trcfilu  24197  neipcfilu  24199  blssps  24328  blss  24329  ssblex  24332  blin2  24333  metss2  24416  metrest  24428  metcnp3  24444  metustexhalf  24460  metustbl  24470  psmetutop  24471  xrsmopn  24717  recld2  24719  icccmplem1  24727  icccmplem2  24728  icccmp  24730  reconnlem2  24732  lebnumlem3  24878  lebnum  24879  xlebnum  24880  lebnumii  24881  nmhmcn  25036  cfilfval  25180  caubl  25224  caublcls  25225  bcthlem1  25240  bcth  25245  ovolfiniun  25418  ovoliunlem3  25421  ovoliun  25422  ovoliun2  25423  ovoliunnul  25424  voliunlem3  25469  dyadmax  25515  dyadmbllem  25516  dyadmbl  25517  opnmbllem  25518  ellimc2  25794  limcnlp  25795  ellimc3  25796  limcflf  25798  limciun  25811  cpnord  25853  lhop  25937  xrlimcnp  26894  cvxcl  26911  dchrval  27161  noetalem2  27670  madebdayim  27820  madebdaylemold  27830  madebday  27832  bdayle  27848  precsexlem8  28139  ausgrumgri  29130  ausgrusgri  29131  nbgrval  29299  nbgrel  29303  nbumgrvtx  29309  nbgrnself  29322  uvtxel1  29359  wlkonl1iedg  29627  crctcshwlkn0lem6  29778  2wlkdlem10  29898  1wlkdlem4  30102  3wlkdlem6  30127  3wlkdlem10  30131  eupth2lem3lem4  30193  frcond1  30228  frgr1v  30233  nfrgr2v  30234  frgr3vlem1  30235  frgr3vlem2  30236  frgr3v  30237  4cycl2vnunb  30252  n4cyclfrgr  30253  isssp  30686  ubthlem1  30832  shmodi  31352  chsupid  31374  chsscon3  31462  spansncvi  31614  mdslmd1lem3  32289  mdslmd1lem4  32290  mdsymlem5  32369  dmdbr5ati  32384  dmdbr6ati  32385  dmdbr7ati  32386  ssiun2sf  32521  fpwrelmapffslem  32688  prodindf  32819  pwrssmgc  32955  fldgenval  33261  unitprodclb  33336  resssra  33559  constrsscn  33706  constrextdg2lem  33714  constrextdg2  33715  txomap  33800  locfinreflem  33806  tpr2rico  33878  pnfneige0  33917  rrhre  33987  dya2icoseg2  34245  omsfval  34261  eulerpartlemt0  34336  eulerpartgbij  34339  eulerpartlemr  34341  eulerpartlemgs2  34347  eulerpartlemn  34348  eulerpart  34349  bnj517  34851  bnj1014  34927  bnj1015  34928  bnj1123  34952  bnj1125  34958  bnj1450  35016  bnj1452  35018  cplgredgex  35093  kur14  35188  cvmliftlem15  35270  cvmlift2lem12  35286  cvmlift2lem13  35287  mclsval  35535  mclsax  35541  mclsppslem  35555  prodeq12sdv  36191  cbvsumdavw2  36268  cbvproddavw2  36269  opnrebl  36293  opnrebl2  36294  ivthALT  36308  neibastop2lem  36333  fnemeet1  36339  filnetlem1  36351  filnetlem4  36354  bj-imdirval3  37157  bj-imdiridlem  37158  rdgssun  37351  lindsadd  37592  lindsenlbs  37594  ptrecube  37599  poimirlem32  37631  opnmbllem0  37635  mblfinlem1  37636  mblfinlem2  37637  mblfinlem3  37638  ovoliunnfl  37641  ex-ovoliunnfl  37642  voliunnfl  37643  totbndbnd  37768  heibor1lem  37788  heiborlem10  37799  scottexf  38147  scott0f  38148  relcnveq2  38296  cnvref4  38317  elrelscnveq2  38469  dfcnvrefrels2  38504  dfcnvrefrel2  38506  symrefref2  38539  lcv1  39019  lfl1dim  39099  lfl1dim2N  39100  paddasslem17  39815  dihglblem6  41319  dochvalr  41336  dochord3  41351  lpolconN  41466  lcfls1lem  41513  mapdffval  41605  mapdfval  41606  mapdsn2  41621  mapd0  41644  lspindp5  41749  mapdh8ab  41756  primrootscoprbij  42075  aks6d1c2  42103  aks6d1c6lem3  42145  aks6d1c6lem5  42150  aks6d1c7lem1  42153  ismrcd1  42671  nacsfix  42685  setindtr  42997  hbtlem6  43102  oaabsb  43267  tfsconcatrnss  43323  naddwordnexlem4  43374  clcnvlem  43596  iunrelexpmin1  43681  iunrelexpmin2  43685  relexp0a  43689  cotrcltrcl  43698  trclimalb2  43699  cotrclrcl  43715  sbcheg  43752  clsk1indlem1  44018  isotone1  44021  isotone2  44022  ntrclsiso  44040  ntrclsk2  44041  k0004lem1  44120  k0004lem3  44122  scottelrankd  44220  mnuop123d  44235  mnuprdlem1  44245  mnuprdlem2  44246  mnuunid  44250  mnurndlem1  44254  modelaxreplem1  44952  modelaxreplem2  44953  modelaxrep  44955  ssdec  45066  iinssd  45109  iinssdf  45117  ssnnf1octb  45172  iooiinicc  45524  iooiinioc  45538  icccncfext  45869  fourierdlem41  46130  meaiininclem  46468  hoidmvlelem3  46579  hoidmvle  46582  opnvonmbllem1  46614  opnvonmbl  46616  iinhoiicclem  46655  smflim  46759  smflimsuplem7  46808  clnbgrval  47807  clnbgrel  47813  sclnbgrel  47832  isubgredg  47851  isubgruhgr  47853  uhgrimisgrgriclem  47915  uhgrimisgrgric  47916  clnbgrgrimlem  47918  clnbgrgrim  47919  isubgr3stgrlem7  47957  uspgrlimlem1  47973  uspgrlimlem2  47974  uspgrlimlem3  47975  uspgrlim  47977  pgnbgreunbgr  48110  uspgrsprf  48131  iinglb  48807  iscnrm3r  48933  iscnrm3l  48936  imassc  49139  setrecseq  49671  setrec1lem4  49676  setrec2fun  49678