Theorem sseq1d 3923

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875

This theorem is referenced by:  sseq12d  3925  eqsstrd  3930  ssiun2s  4937  disjxiun  5029  treq  5144  iunopeqop  5380  preddowncl  6153  funimass1  6417  feq1  6479  fvmptss  6771  fvimacnvi  6813  fvimacnvALT  6818  knatar  7104  ovmptss  7793  fnsuppres  7865  imacosuppOLD  7885  wrecseq123  7958  wfrlem1  7964  wfrlem3  7966  wfrdmcl  7973  wfrlem15  7979  wfrlem17  7981  dfrecs3  8019  oaordi  8182  oaword2  8189  oawordeulem  8190  omword1  8209  oewordri  8228  oeordsuc  8230  nnaordi  8254  nnawordex  8273  ereq1  8306  elpm2r  8434  inficl  8922  fipwss  8926  dffi3  8928  hartogslem1  9039  inf3lema  9120  inf3lemd  9123  cantnfle  9167  cantnflem2  9186  trcl  9203  tcmin  9216  rankr1ai  9260  rankxplim  9341  scottex  9347  scott0  9348  scottexs  9349  scott0s  9350  karden  9357  cardne  9427  cardaleph  9549  ackbij2  9703  cflim2  9723  cfslb  9726  coftr  9733  fin23lem15  9794  fin23lem32  9804  fin23lem34  9806  fin23lem35  9807  fin23lem36  9808  fin23lem41  9812  isf32lem1  9813  itunitc1  9880  axdc3lem2  9911  ttukeylem1  9969  fpwwe2cbv  10090  fpwwe2lem2  10092  fpwwe2  10103  fpwwecbv  10104  fpwwelem  10105  canthwelem  10110  canthwe  10111  wunex2  10198  wuncval2  10207  eltsk2g  10211  tskpwss  10212  inar1  10235  grothpw  10286  grothpwex  10287  axgroth6  10288  grothac  10290  peano5uzti  12111  fsuppmapnn0fiub0  13410  relexpnndm  14448  rtrclreclem4  14468  dfrtrcl2  14469  lo1o1  14937  o1lo1  14942  o1lo12  14943  lo1eq  14973  rlimeq  14974  isercoll  15072  prmreclem4  16310  vdwmc  16369  vdwlem1  16372  vdwlem2  16373  vdwlem12  16383  vdwlem13  16384  ramval  16399  ramz2  16415  ramub1lem1  16417  isacs2  16982  isacs1i  16986  mreacs  16987  acsfn  16988  rescabs  17162  ipole  17834  ipodrsima  17841  isacs5  17848  symgsssg  18662  psgnunilem5  18689  sylow1  18795  efgval2  18917  efgsfo  18932  frgpuplem  18965  gsumzf1o  19100  gsumzoppg  19132  dprdcntz  19198  islbs2  19994  frlmssuvc1  20559  frlmssuvc2  20560  frlmsslsp  20561  ismhp  20884  pptbas  21708  pnfnei  21920  mnfnei  21921  iscnp  21937  iscnp4  21963  cnntr  21975  cnconst2  21983  cnpresti  21988  cnprest  21989  isreg  22032  isnrm  22035  isnrm2  22058  perfcls  22065  isreg2  22077  hauscmplem  22106  1stcfb  22145  1stcelcls  22161  1stccnp  22162  txbas  22267  ptbasfi  22281  xkoopn  22289  xkoccn  22319  txcnp  22320  ptcnplem  22321  txdis  22332  txdis1cn  22335  txtube  22340  txkgen  22352  xkohaus  22353  xkoptsub  22354  xkoco1cn  22357  xkoco2cn  22358  xkococnlem  22359  xkococn  22360  xkoinjcn  22387  kqreglem1  22441  kqreglem2  22442  kqnrmlem1  22443  kqnrmlem2  22444  reghmph  22493  nrmhmph  22494  trfil2  22587  ufileu  22619  elfm  22647  elfm2  22648  elfm3  22650  imaelfm  22651  rnelfm  22653  fmfnfmlem2  22655  fmfnfmlem4  22657  fmco  22661  elflim2  22664  flffbas  22695  lmflf  22705  txflf  22706  fclscf  22725  flimfnfcls  22728  cnextcn  22767  symgtgp  22806  ghmcnp  22815  qustgplem  22821  eltsms  22833  ustval  22903  ust0  22920  trust  22930  utoptop  22935  restutop  22938  restutopopn  22939  utopsnneiplem  22948  ucncn  22986  fmucnd  22993  cfilufg  22994  trcfilu  22995  neipcfilu  22997  blssps  23126  blss  23127  ssblex  23130  blin2  23131  metss2  23214  metrest  23226  metcnp3  23242  metustexhalf  23258  metustbl  23268  psmetutop  23269  xrsmopn  23513  recld2  23515  icccmplem1  23523  icccmplem2  23524  icccmp  23526  reconnlem2  23528  lebnumlem3  23664  lebnum  23665  xlebnum  23666  lebnumii  23667  nmhmcn  23821  cfilfval  23964  caubl  24008  caublcls  24009  bcthlem1  24024  bcth  24029  ovolfiniun  24201  ovoliunlem3  24204  ovoliun  24205  ovoliun2  24206  ovoliunnul  24207  voliunlem3  24252  dyadmax  24298  dyadmbllem  24299  dyadmbl  24300  opnmbllem  24301  ellimc2  24576  limcnlp  24577  ellimc3  24578  limcflf  24580  limciun  24593  cpnord  24634  lhop  24715  xrlimcnp  25653  cvxcl  25669  dchrval  25917  ausgrumgri  27059  ausgrusgri  27060  nbgrval  27225  nbgrel  27229  nbumgrvtx  27235  nbgrnself  27248  uvtxel1  27285  wlkonl1iedg  27554  crctcshwlkn0lem6  27700  2wlkdlem10  27820  1wlkdlem4  28024  3wlkdlem6  28049  3wlkdlem10  28053  eupth2lem3lem4  28115  frcond1  28150  frgr1v  28155  nfrgr2v  28156  frgr3vlem1  28157  frgr3vlem2  28158  frgr3v  28159  4cycl2vnunb  28174  n4cyclfrgr  28175  isssp  28606  ubthlem1  28752  shmodi  29272  chsupid  29294  chsscon3  29382  spansncvi  29534  mdslmd1lem3  30209  mdslmd1lem4  30210  mdsymlem5  30289  dmdbr5ati  30304  dmdbr6ati  30305  dmdbr7ati  30306  ssiun2sf  30421  fpwrelmapffslem  30591  pwrssmgc  30804  txomap  31305  locfinreflem  31311  tpr2rico  31383  pnfneige0  31422  rrhre  31490  prodindf  31510  dya2icoseg2  31764  omsfval  31780  eulerpartlemt0  31855  eulerpartgbij  31858  eulerpartlemr  31860  eulerpartlemgs2  31866  eulerpartlemn  31867  eulerpart  31868  bnj517  32385  bnj1014  32461  bnj1015  32462  bnj1123  32486  bnj1125  32492  bnj1450  32550  bnj1452  32552  cplgredgex  32598  kur14  32694  cvmliftlem15  32776  cvmlift2lem12  32792  cvmlift2lem13  32793  mclsval  33041  mclsax  33047  mclsppslem  33061  dfpo2  33238  trpredlem1  33313  trpredmintr  33317  frecseq123  33380  frrlem1  33384  frrlem3  33386  frrlem4  33387  frrlem13  33396  noetalem2  33510  madebdayim  33627  madebdaylemold  33635  madebday  33637  opnrebl  34058  opnrebl2  34059  ivthALT  34073  neibastop2lem  34098  fnemeet1  34104  filnetlem1  34116  filnetlem4  34119  bj-imdirval3  34879  bj-imdiridlem  34880  csbwrecsg  35024  rdgssun  35075  lindsadd  35330  lindsenlbs  35332  ptrecube  35337  poimirlem32  35369  opnmbllem0  35373  mblfinlem1  35374  mblfinlem2  35375  mblfinlem3  35376  ovoliunnfl  35379  ex-ovoliunnfl  35380  voliunnfl  35381  totbndbnd  35507  heibor1lem  35527  heiborlem10  35538  scottexf  35886  scott0f  35887  relcnveq2  36020  elrelscnveq2  36173  dfcnvrefrels2  36206  dfcnvrefrel2  36208  symrefref2  36239  lcv1  36617  lfl1dim  36697  lfl1dim2N  36698  paddasslem17  37412  dihglblem6  38916  dochvalr  38933  dochord3  38948  lpolconN  39063  lcfls1lem  39110  mapdffval  39202  mapdfval  39203  mapdsn2  39218  mapd0  39241  lspindp5  39346  mapdh8ab  39353  ismrcd1  40012  nacsfix  40026  setindtr  40338  hbtlem6  40446  clcnvlem  40696  iunrelexpmin1  40782  iunrelexpmin2  40786  relexp0a  40790  cotrcltrcl  40799  trclimalb2  40800  cotrclrcl  40816  sbcheg  40853  clsk1indlem1  41121  isotone1  41124  isotone2  41125  ntrclsiso  41143  ntrclsk2  41144  k0004lem1  41223  k0004lem3  41225  scottelrankd  41328  mnuop123d  41343  mnuprdlem1  41353  mnuprdlem2  41354  mnuunid  41358  mnurndlem1  41362  ssdec  42097  iinssd  42139  iinssdf  42147  ssnnf1octb  42192  iooiinicc  42545  iooiinioc  42559  icccncfext  42895  fourierdlem41  43156  meaiininclem  43491  hoidmvlelem3  43602  hoidmvle  43605  opnvonmbllem1  43637  opnvonmbl  43639  iinhoiicclem  43678  smflim  43776  smflimsuplem7  43823  uspgrsprf  44741  setrecseq  45606  setrec1lem4  45611  setrec2fun  45613