Theorem sseq1d 3967

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sseq12d  3969  eqsstrd  3970  ssiun2s  5005  disjxiun  5096  treq  5213  iunopeqop  5489  iunopeqopOLD  5490  dfpo2  6279  preddowncl  6315  funimass1  6599  f1imadifssran  6603  feq1  6665  focofo  6787  fvmptss  6984  fvimacnvi  7029  fvimacnvALT  7034  knatar  7337  ovmptss  8067  fnsuppres  8166  frecseq123  8258  csbfrecsg  8260  frrlem1  8262  frrlem3  8264  frrlem4  8265  frrlem13  8274  frrdmcl  8284  fprresex  8286  dfrecs3  8338  oaordi  8510  oaword2  8517  oawordeulem  8518  omword1  8537  oewordri  8557  oeordsuc  8559  nnaordi  8583  nnawordex  8602  naddcllem  8641  naddunif  8659  ereq1  8681  elpm2r  8822  inficl  9368  fipwss  9372  dffi3  9374  hartogslem1  9487  inf3lema  9576  inf3lemd  9579  cantnfle  9623  cantnflem2  9642  ttrclselem1  9677  trcl  9680  tcmin  9691  rankr1ai  9753  rankxplim  9834  scottex  9840  scott0  9841  scottexs  9842  scott0s  9843  karden  9850  cardne  9920  cardaleph  10042  ackbij2  10195  cflim2  10217  cfslb  10220  coftr  10227  fin23lem15  10288  fin23lem32  10298  fin23lem34  10300  fin23lem35  10301  fin23lem36  10302  fin23lem41  10306  isf32lem1  10307  itunitc1  10374  axdc3lem2  10405  ttukeylem1  10463  fpwwe2cbv  10585  fpwwe2lem2  10587  fpwwe2lem4  10589  fpwwe2  10598  fpwwecbv  10599  fpwwelem  10600  canthwelem  10605  canthwe  10606  pwfseqlem4  10617  wunex2  10693  wuncval2  10702  eltsk2g  10706  tskpwss  10707  inar1  10730  grothpw  10781  grothpwex  10782  axgroth6  10783  grothac  10785  peano5uzti  12660  fsuppmapnn0fiub0  14003  relexpnndm  15051  rtrclreclem4  15071  dfrtrcl2  15072  lo1o1  15542  o1lo1  15547  o1lo12  15548  lo1eq  15578  rlimeq  15579  isercoll  15678  prmreclem4  16938  vdwmc  16997  vdwlem1  17000  vdwlem2  17001  vdwlem12  17011  vdwlem13  17012  ramval  17027  ramz2  17043  ramub1lem1  17045  isacs2  17668  isacs1i  17672  mreacs  17673  acsfn  17674  rescabs  17849  ipole  18549  ipodrsima  18556  isacs5  18563  symgsssg  19490  psgnunilem5  19517  sylow1  19626  efgval2  19747  efgsfo  19762  frgpuplem  19795  gsumzf1o  19935  gsumzoppg  19967  dprdcntz  20033  islbs2  21204  frlmssuvc1  21826  frlmssuvc2  21827  frlmsslsp  21828  ismhp  22185  pptbas  23048  pnfnei  23260  mnfnei  23261  iscnp  23277  iscnp4  23303  cnntr  23315  cnconst2  23323  cnpresti  23328  cnprest  23329  isreg  23372  isnrm  23375  isnrm2  23398  perfcls  23405  isreg2  23417  hauscmplem  23446  1stcfb  23485  1stcelcls  23501  1stccnp  23502  txbas  23607  ptbasfi  23621  xkoopn  23629  xkoccn  23659  txcnp  23660  ptcnplem  23661  txdis  23672  txdis1cn  23675  txtube  23680  txkgen  23692  xkohaus  23693  xkoptsub  23694  xkoco1cn  23697  xkoco2cn  23698  xkococnlem  23699  xkococn  23700  xkoinjcn  23727  kqreglem1  23781  kqreglem2  23782  kqnrmlem1  23783  kqnrmlem2  23784  reghmph  23833  nrmhmph  23834  trfil2  23927  ufileu  23959  elfm  23987  elfm2  23988  elfm3  23990  imaelfm  23991  rnelfm  23993  fmfnfmlem2  23995  fmfnfmlem4  23997  fmco  24001  elflim2  24004  flffbas  24035  lmflf  24045  txflf  24046  fclscf  24065  flimfnfcls  24068  cnextcn  24107  symgtgp  24146  ghmcnp  24155  qustgplem  24161  eltsms  24173  ustval  24243  ust0  24260  trust  24269  utoptop  24274  restutop  24277  restutopopn  24278  utopsnneiplem  24287  ucncn  24324  fmucnd  24331  cfilufg  24332  trcfilu  24333  neipcfilu  24335  blssps  24464  blss  24465  ssblex  24468  blin2  24469  metss2  24552  metrest  24564  metcnp3  24580  metustexhalf  24596  metustbl  24606  psmetutop  24607  xrsmopn  24853  recld2  24855  icccmplem1  24863  icccmplem2  24864  icccmp  24866  reconnlem2  24868  lebnumlem3  25005  lebnum  25006  xlebnum  25007  lebnumii  25008  nmhmcn  25162  cfilfval  25306  caubl  25350  caublcls  25351  bcthlem1  25366  bcth  25371  ovolfiniun  25543  ovoliunlem3  25546  ovoliun  25547  ovoliun2  25548  ovoliunnul  25549  voliunlem3  25594  dyadmax  25640  dyadmbllem  25641  dyadmbl  25642  opnmbllem  25643  ellimc2  25919  limcnlp  25920  ellimc3  25921  limcflf  25923  limciun  25936  cpnord  25977  lhop  26058  xrlimcnp  27010  cvxcl  27026  dchrval  27275  noetalem2  27783  madebdayim  27958  madebdaylemold  27968  madebday  27970  bdayle  27986  precsexlem8  28284  bdaypw2n0bndlem  28533  bdayfinbndcbv  28536  bdayfinbndlem1  28537  bdayfinbndlem2  28538  bdayfinbnd  28539  ausgrumgri  29314  ausgrusgri  29315  nbgrval  29483  nbgrel  29487  nbumgrvtx  29493  nbgrnself  29506  uvtxel1  29543  wlkonl1iedg  29810  crctcshwlkn0lem6  29961  2wlkdlem10  30081  1wlkdlem4  30288  3wlkdlem6  30313  3wlkdlem10  30317  eupth2lem3lem4  30379  frcond1  30414  frgr1v  30419  nfrgr2v  30420  frgr3vlem1  30421  frgr3vlem2  30422  frgr3v  30423  4cycl2vnunb  30438  n4cyclfrgr  30439  isssp  30873  ubthlem1  31019  shmodi  31539  chsupid  31561  chsscon3  31649  spansncvi  31801  mdslmd1lem3  32476  mdslmd1lem4  32477  mdsymlem5  32556  dmdbr5ati  32571  dmdbr6ati  32572  dmdbr7ati  32573  ssiun2sf  32708  fpwrelmapffslem  32884  prodindf  33001  pwrssmgc  33139  fldgenval  33460  unitprodclb  33536  esplysply  33829  esplyfvaln  33832  esplyind  33833  resssra  33845  constrsscn  33998  constrextdg2lem  34006  constrextdg2  34007  txomap  34092  locfinreflem  34098  tpr2rico  34170  pnfneige0  34209  rrhre  34279  dya2icoseg2  34536  omsfval  34552  eulerpartlemt0  34627  eulerpartgbij  34630  eulerpartlemr  34632  eulerpartlemgs2  34638  eulerpartlemn  34639  eulerpart  34640  bnj517  35144  bnj1014  35220  bnj1015  35221  bnj1123  35245  bnj1125  35251  bnj1450  35309  bnj1452  35311  cplgredgex  35435  kur14  35530  cvmliftlem15  35612  cvmlift2lem12  35628  cvmlift2lem13  35629  mclsval  35877  mclsax  35883  mclsppslem  35897  prodeq12sdv  36542  cbvsumdavw2  36619  cbvproddavw2  36620  opnrebl  36644  opnrebl2  36645  ivthALT  36659  neibastop2lem  36684  fnemeet1  36690  filnetlem1  36702  filnetlem4  36705  ttcmin  36820  dfttc2g  36830  bj-imdirval3  37640  bj-imdiridlem  37641  rdgssun  37836  lindsadd  38076  lindsenlbs  38078  ptrecube  38083  poimirlem32  38115  opnmbllem0  38119  mblfinlem1  38120  mblfinlem2  38121  mblfinlem3  38122  ovoliunnfl  38125  ex-ovoliunnfl  38126  voliunnfl  38127  totbndbnd  38252  heibor1lem  38272  heiborlem10  38283  scottexf  38631  scott0f  38632  relcnveq2  38792  cnvref4  38813  dfcnvrefrels2  39071  dfcnvrefrel2  39073  elrelscnveq2  39092  symrefref2  39110  lcv1  39629  lfl1dim  39709  lfl1dim2N  39710  paddasslem17  40424  dihglblem6  41928  dochvalr  41945  dochord3  41960  lpolconN  42075  lcfls1lem  42122  mapdffval  42214  mapdfval  42215  mapdsn2  42230  mapd0  42253  lspindp5  42358  mapdh8ab  42365  primrootscoprbij  42683  aks6d1c2  42711  aks6d1c6lem3  42753  aks6d1c6lem5  42758  aks6d1c7lem1  42761  ismrcd1  43243  nacsfix  43257  setindtr  43565  hbtlem6  43670  oaabsb  43835  tfsconcatrnss  43891  naddwordnexlem4  43942  clcnvlem  44163  iunrelexpmin1  44248  iunrelexpmin2  44252  relexp0a  44256  cotrcltrcl  44265  trclimalb2  44266  cotrclrcl  44282  sbcheg  44319  clsk1indlem1  44585  isotone1  44588  isotone2  44589  ntrclsiso  44607  ntrclsk2  44608  k0004lem1  44687  k0004lem3  44689  scottelrankd  44787  mnuop123d  44802  mnuprdlem1  44812  mnuprdlem2  44813  mnuunid  44817  mnurndlem1  44821  modelaxreplem1  45518  modelaxreplem2  45519  modelaxrep  45521  ssdec  45630  iinssd  45673  iinssdf  45681  ssnnf1octb  45736  iooiinicc  46082  iooiinioc  46096  icccncfext  46425  fourierdlem41  46686  meaiininclem  47024  hoidmvlelem3  47135  hoidmvle  47138  opnvonmbllem1  47170  opnvonmbl  47172  iinhoiicclem  47211  smflim  47315  smflimsuplem7  47364  clnbgrval  48408  clnbgrel  48414  sclnbgrel  48433  isubgredg  48452  isubgruhgr  48454  uhgrimisgrgriclem  48516  uhgrimisgrgric  48517  clnbgrgrimlem  48519  clnbgrgrim  48520  isubgr3stgrlem7  48558  uspgrlimlem1  48574  uspgrlimlem2  48575  uspgrlimlem3  48576  uspgrlim  48578  pgnbgreunbgr  48711  uspgrsprf  48732  iinglb  49407  iscnrm3r  49533  iscnrm3l  49536  imassc  49738  setrecseq  50270  setrec1lem4  50275  setrec2fun  50277