Theorem sseq1d 3948

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseq12d  3950  eqsstrd  3955  ssiun2s  4974  disjxiun  5067  treq  5193  iunopeqop  5429  dfpo2  6188  preddowncl  6224  funimass1  6500  feq1  6565  focofo  6685  fvmptss  6869  fvimacnvi  6911  fvimacnvALT  6916  knatar  7208  ovmptss  7904  fnsuppres  7978  frecseq123  8069  csbfrecsg  8071  frrlem1  8073  frrlem3  8075  frrlem4  8076  frrlem13  8085  frrdmcl  8095  fprresex  8097  wrecseq123OLD  8102  wfrlem1OLD  8110  wfrlem3OLD  8112  wfrdmclOLD  8119  wfrlem15OLD  8125  wfrlem17OLD  8127  dfrecs3  8174  dfrecs3OLD  8175  oaordi  8339  oaword2  8346  oawordeulem  8347  omword1  8366  oewordri  8385  oeordsuc  8387  nnaordi  8411  nnawordex  8430  ereq1  8463  elpm2r  8591  inficl  9114  fipwss  9118  dffi3  9120  hartogslem1  9231  inf3lema  9312  inf3lemd  9315  cantnfle  9359  cantnflem2  9378  trpredlem1  9405  trpredmintr  9409  trcl  9417  tcmin  9430  rankr1ai  9487  rankxplim  9568  scottex  9574  scott0  9575  scottexs  9576  scott0s  9577  karden  9584  cardne  9654  cardaleph  9776  ackbij2  9930  cflim2  9950  cfslb  9953  coftr  9960  fin23lem15  10021  fin23lem32  10031  fin23lem34  10033  fin23lem35  10034  fin23lem36  10035  fin23lem41  10039  isf32lem1  10040  itunitc1  10107  axdc3lem2  10138  ttukeylem1  10196  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwe2  10330  fpwwecbv  10331  fpwwelem  10332  canthwelem  10337  canthwe  10338  wunex2  10425  wuncval2  10434  eltsk2g  10438  tskpwss  10439  inar1  10462  grothpw  10513  grothpwex  10514  axgroth6  10515  grothac  10517  peano5uzti  12340  fsuppmapnn0fiub0  13641  relexpnndm  14680  rtrclreclem4  14700  dfrtrcl2  14701  lo1o1  15169  o1lo1  15174  o1lo12  15175  lo1eq  15205  rlimeq  15206  isercoll  15307  prmreclem4  16548  vdwmc  16607  vdwlem1  16610  vdwlem2  16611  vdwlem12  16621  vdwlem13  16622  ramval  16637  ramz2  16653  ramub1lem1  16655  isacs2  17279  isacs1i  17283  mreacs  17284  acsfn  17285  rescabs  17464  ipole  18167  ipodrsima  18174  isacs5  18181  symgsssg  18990  psgnunilem5  19017  sylow1  19123  efgval2  19245  efgsfo  19260  frgpuplem  19293  gsumzf1o  19428  gsumzoppg  19460  dprdcntz  19526  islbs2  20331  frlmssuvc1  20911  frlmssuvc2  20912  frlmsslsp  20913  ismhp  21241  pptbas  22066  pnfnei  22279  mnfnei  22280  iscnp  22296  iscnp4  22322  cnntr  22334  cnconst2  22342  cnpresti  22347  cnprest  22348  isreg  22391  isnrm  22394  isnrm2  22417  perfcls  22424  isreg2  22436  hauscmplem  22465  1stcfb  22504  1stcelcls  22520  1stccnp  22521  txbas  22626  ptbasfi  22640  xkoopn  22648  xkoccn  22678  txcnp  22679  ptcnplem  22680  txdis  22691  txdis1cn  22694  txtube  22699  txkgen  22711  xkohaus  22712  xkoptsub  22713  xkoco1cn  22716  xkoco2cn  22717  xkococnlem  22718  xkococn  22719  xkoinjcn  22746  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  reghmph  22852  nrmhmph  22853  trfil2  22946  ufileu  22978  elfm  23006  elfm2  23007  elfm3  23009  imaelfm  23010  rnelfm  23012  fmfnfmlem2  23014  fmfnfmlem4  23016  fmco  23020  elflim2  23023  flffbas  23054  lmflf  23064  txflf  23065  fclscf  23084  flimfnfcls  23087  cnextcn  23126  symgtgp  23165  ghmcnp  23174  qustgplem  23180  eltsms  23192  ustval  23262  ust0  23279  trust  23289  utoptop  23294  restutop  23297  restutopopn  23298  utopsnneiplem  23307  ucncn  23345  fmucnd  23352  cfilufg  23353  trcfilu  23354  neipcfilu  23356  blssps  23485  blss  23486  ssblex  23489  blin2  23490  metss2  23574  metrest  23586  metcnp3  23602  metustexhalf  23618  metustbl  23628  psmetutop  23629  xrsmopn  23881  recld2  23883  icccmplem1  23891  icccmplem2  23892  icccmp  23894  reconnlem2  23896  lebnumlem3  24032  lebnum  24033  xlebnum  24034  lebnumii  24035  nmhmcn  24189  cfilfval  24333  caubl  24377  caublcls  24378  bcthlem1  24393  bcth  24398  ovolfiniun  24570  ovoliunlem3  24573  ovoliun  24574  ovoliun2  24575  ovoliunnul  24576  voliunlem3  24621  dyadmax  24667  dyadmbllem  24668  dyadmbl  24669  opnmbllem  24670  ellimc2  24946  limcnlp  24947  ellimc3  24948  limcflf  24950  limciun  24963  cpnord  25004  lhop  25085  xrlimcnp  26023  cvxcl  26039  dchrval  26287  ausgrumgri  27440  ausgrusgri  27441  nbgrval  27606  nbgrel  27610  nbumgrvtx  27616  nbgrnself  27629  uvtxel1  27666  wlkonl1iedg  27935  crctcshwlkn0lem6  28081  2wlkdlem10  28201  1wlkdlem4  28405  3wlkdlem6  28430  3wlkdlem10  28434  eupth2lem3lem4  28496  frcond1  28531  frgr1v  28536  nfrgr2v  28537  frgr3vlem1  28538  frgr3vlem2  28539  frgr3v  28540  4cycl2vnunb  28555  n4cyclfrgr  28556  isssp  28987  ubthlem1  29133  shmodi  29653  chsupid  29675  chsscon3  29763  spansncvi  29915  mdslmd1lem3  30590  mdslmd1lem4  30591  mdsymlem5  30670  dmdbr5ati  30685  dmdbr6ati  30686  dmdbr7ati  30687  ssiun2sf  30800  fpwrelmapffslem  30969  pwrssmgc  31180  txomap  31686  locfinreflem  31692  tpr2rico  31764  pnfneige0  31803  rrhre  31871  prodindf  31891  dya2icoseg2  32145  omsfval  32161  eulerpartlemt0  32236  eulerpartgbij  32239  eulerpartlemr  32241  eulerpartlemgs2  32247  eulerpartlemn  32248  eulerpart  32249  bnj517  32765  bnj1014  32841  bnj1015  32842  bnj1123  32866  bnj1125  32872  bnj1450  32930  bnj1452  32932  cplgredgex  32982  kur14  33078  cvmliftlem15  33160  cvmlift2lem12  33176  cvmlift2lem13  33177  mclsval  33425  mclsax  33431  mclsppslem  33445  ttrclselem1  33711  naddcllem  33758  noetalem2  33872  madebdayim  33997  madebdaylemold  34005  madebday  34007  opnrebl  34436  opnrebl2  34437  ivthALT  34451  neibastop2lem  34476  fnemeet1  34482  filnetlem1  34494  filnetlem4  34497  bj-imdirval3  35282  bj-imdiridlem  35283  rdgssun  35476  lindsadd  35697  lindsenlbs  35699  ptrecube  35704  poimirlem32  35736  opnmbllem0  35740  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  ovoliunnfl  35746  ex-ovoliunnfl  35747  voliunnfl  35748  totbndbnd  35874  heibor1lem  35894  heiborlem10  35905  scottexf  36253  scott0f  36254  relcnveq2  36385  elrelscnveq2  36538  dfcnvrefrels2  36571  dfcnvrefrel2  36573  symrefref2  36604  lcv1  36982  lfl1dim  37062  lfl1dim2N  37063  paddasslem17  37777  dihglblem6  39281  dochvalr  39298  dochord3  39313  lpolconN  39428  lcfls1lem  39475  mapdffval  39567  mapdfval  39568  mapdsn2  39583  mapd0  39606  lspindp5  39711  mapdh8ab  39718  ismrcd1  40436  nacsfix  40450  setindtr  40762  hbtlem6  40870  clcnvlem  41120  iunrelexpmin1  41205  iunrelexpmin2  41209  relexp0a  41213  cotrcltrcl  41222  trclimalb2  41223  cotrclrcl  41239  sbcheg  41276  clsk1indlem1  41544  isotone1  41547  isotone2  41548  ntrclsiso  41566  ntrclsk2  41567  k0004lem1  41646  k0004lem3  41648  scottelrankd  41754  mnuop123d  41769  mnuprdlem1  41779  mnuprdlem2  41780  mnuunid  41784  mnurndlem1  41788  ssdec  42527  iinssd  42569  iinssdf  42577  ssnnf1octb  42622  iooiinicc  42970  iooiinioc  42984  icccncfext  43318  fourierdlem41  43579  meaiininclem  43914  hoidmvlelem3  44025  hoidmvle  44028  opnvonmbllem1  44060  opnvonmbl  44062  iinhoiicclem  44101  smflim  44199  smflimsuplem7  44246  uspgrsprf  45196  iscnrm3r  46130  iscnrm3l  46133  setrecseq  46277  setrec1lem4  46282  setrec2fun  46284