Theorem sseq1d 3595

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sseq12d  3597  eqsstrd  3602  snssg  4268  ssiun2s  4500  disjxiun  4579  disjxiunOLD  4580  treq  4686  iunopeqop  4906  preddowncl  5624  funimass1  5885  feq1  5939  fvmptss  6201  fvimacnvi  6239  fvimacnvALT  6244  knatar  6507  ovmptss  7145  fnsuppres  7209  imacosupp  7222  wrecseq123  7295  wfrlem1  7301  wfrlem3  7303  wfrdmcl  7310  wfrlem15  7316  wfrlem17  7318  dfrecs3  7356  oaordi  7513  oaword2  7520  oawordeulem  7521  omword1  7540  oewordri  7559  oeordsuc  7561  nnaordi  7585  nnawordex  7604  ereq1  7636  elpm2r  7761  inficl  8214  fipwss  8218  dffi3  8220  hartogslem1  8330  inf3lema  8404  inf3lemd  8407  cantnfle  8451  cantnflem2  8470  trcl  8487  tcmin  8500  rankr1ai  8544  rankxplim  8625  scottex  8631  scott0  8632  scottexs  8633  scott0s  8634  karden  8641  cardne  8674  cardaleph  8795  ackbij2  8948  cflim2  8968  cfslb  8971  coftr  8978  fin23lem15  9039  fin23lem32  9049  fin23lem34  9051  fin23lem35  9052  fin23lem36  9053  fin23lem41  9057  isf32lem1  9058  itunitc1  9125  axdc3lem2  9156  ttukeylem1  9214  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwe2  9344  fpwwecbv  9345  fpwwelem  9346  canthwelem  9351  canthwe  9352  wunex2  9439  wuncval2  9448  eltsk2g  9452  tskpwss  9453  inar1  9476  grothpw  9527  grothpwex  9528  axgroth6  9529  grothac  9531  peano5uzti  11343  fsuppmapnn0fiub0  12655  relexpnndm  13629  rtrclreclem4  13649  dfrtrcl2  13650  lo1o1  14111  o1lo1  14116  o1lo12  14117  lo1eq  14147  rlimeq  14148  isercoll  14246  prmreclem4  15461  vdwmc  15520  vdwlem1  15523  vdwlem2  15524  vdwlem12  15534  vdwlem13  15535  ramval  15550  ramz2  15566  ramub1lem1  15568  isacs2  16137  isacs1i  16141  mreacs  16142  acsfn  16143  rescabs  16316  ipole  16981  ipodrsima  16988  isacs5  16995  symgsssg  17710  psgnunilem5  17737  sylow1  17841  efgval2  17960  efgsfo  17975  frgpuplem  18008  gsumzf1o  18136  gsumzoppg  18167  dprdcntz  18230  islbs2  18975  frlmssuvc1  19952  frlmssuvc2  19953  frlmsslsp  19954  pptbas  20622  pnfnei  20834  mnfnei  20835  iscnp  20851  iscnp4  20877  cnntr  20889  cnconst2  20897  cnpresti  20902  cnprest  20903  isreg  20946  isnrm  20949  isnrm2  20972  perfcls  20979  isreg2  20991  hauscmplem  21019  1stcfb  21058  1stcelcls  21074  1stccnp  21075  txbas  21180  ptbasfi  21194  xkoopn  21202  xkoccn  21232  txcnp  21233  ptcnplem  21234  txdis  21245  txdis1cn  21248  txtube  21253  txkgen  21265  xkohaus  21266  xkoptsub  21267  xkoco1cn  21270  xkoco2cn  21271  xkococnlem  21272  xkococn  21273  xkoinjcn  21300  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  reghmph  21406  nrmhmph  21407  trfil2  21501  ufileu  21533  elfm  21561  elfm2  21562  elfm3  21564  imaelfm  21565  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fmco  21575  elflim2  21578  flffbas  21609  lmflf  21619  txflf  21620  fclscf  21639  flimfnfcls  21642  cnextcn  21681  symgtgp  21715  ghmcnp  21728  qustgplem  21734  eltsms  21746  ustval  21816  ust0  21833  trust  21843  utoptop  21848  restutop  21851  restutopopn  21852  utopsnneiplem  21861  ucncn  21899  fmucnd  21906  cfilufg  21907  trcfilu  21908  neipcfilu  21910  blssps  22039  blss  22040  ssblex  22043  blin2  22044  metss2  22127  metrest  22139  metcnp3  22155  metustexhalf  22171  metustbl  22181  psmetutop  22182  xrsmopn  22423  recld2  22425  icccmplem1  22433  icccmplem2  22434  icccmp  22436  reconnlem2  22438  lebnumlem3  22570  lebnum  22571  xlebnum  22572  lebnumii  22573  nmhmcn  22728  cfilfval  22870  caubl  22914  caublcls  22915  bcthlem1  22929  bcth  22934  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  ovoliunnul  23082  voliunlem3  23127  dyadmax  23172  dyadmbllem  23173  dyadmbl  23174  opnmbllem  23175  ellimc2  23447  limcnlp  23448  ellimc3  23449  limcflf  23451  limciun  23464  cpnord  23504  lhop  23583  xrlimcnp  24495  cvxcl  24511  dchrval  24759  frgraunss  26522  frgra1v  26525  frgra2v  26526  frgra3vlem1  26527  frgra3vlem2  26528  frgra3v  26529  4cycl2vnunb  26544  n4cyclfrgra  26545  isssp  26963  ubthlem1  27110  shmodi  27633  chsupid  27655  chsscon3  27743  spansncvi  27895  mdslmd1lem3  28570  mdslmd1lem4  28571  mdsymlem5  28650  dmdbr5ati  28665  dmdbr6ati  28666  dmdbr7ati  28667  ssiun2sf  28760  fpwrelmapffslem  28895  txomap  29229  locfinreflem  29235  tpr2rico  29286  pnfneige0  29325  rrhre  29393  dya2icoseg2  29667  omsfval  29683  eulerpartlemt0  29758  eulerpartgbij  29761  eulerpartlemr  29763  eulerpartlemgs2  29769  eulerpartlemn  29770  eulerpart  29771  bnj517  30209  bnj1014  30284  bnj1015  30285  bnj1123  30308  bnj1125  30314  bnj1450  30372  bnj1452  30374  kur14  30452  cvmliftlem15  30534  cvmlift2lem12  30550  cvmlift2lem13  30551  mclsval  30714  mclsax  30720  mclsppslem  30734  dfpo2  30898  trpredlem1  30971  trpredmintr  30975  frrlem1  31024  frrlem4  31027  frrlem5e  31032  nobndup  31099  nobnddown  31100  nofulllem5  31105  opnrebl  31485  opnrebl2  31486  ivthALT  31500  neibastop2lem  31525  fnemeet1  31531  filnetlem1  31543  filnetlem4  31546  csbwrecsg  32349  lindsenlbs  32574  ptrecube  32579  poimirlem32  32611  opnmbllem0  32615  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  ovoliunnfl  32621  ex-ovoliunnfl  32622  voliunnfl  32623  totbndbnd  32758  heibor1lem  32778  heiborlem10  32789  scottexf  33146  scott0f  33147  lcv1  33346  lfl1dim  33426  lfl1dim2N  33427  paddasslem17  34140  dihglblem6  35647  dochvalr  35664  dochord3  35679  lpolconN  35794  lcfls1lem  35841  mapdffval  35933  mapdfval  35934  mapdsn2  35949  mapd0  35972  lspindp5  36077  mapdh8ab  36084  ismrcd1  36279  nacsfix  36293  setindtr  36609  hbtlem6  36718  clcnvlem  36949  iunrelexpmin1  37019  iunrelexpmin2  37023  relexp0a  37027  cotrcltrcl  37036  trclimalb2  37037  cotrclrcl  37053  sbcheg  37093  clsk1indlem1  37363  isotone1  37366  isotone2  37367  ntrclsiso  37385  ntrclsk2  37386  k0004lem1  37465  k0004lem3  37467  ssdec  38293  ssnnf1octb  38377  iooiinicc  38616  iooiinioc  38630  icccncfext  38773  fourierdlem41  39041  meaiininclem  39376  hoidmvlelem3  39487  hoidmvle  39490  opnvonmbllem1  39522  opnvonmbl  39524  iinhoiicclem  39564  smflim  39663  ausgrumgri  40397  ausgrusgri  40398  nbgrval  40560  nbgrel  40564  nbumgrvtx  40568  nbgrnself  40583  uvtxael1  40622  wlkOnl1iedg  40873  crctcsh1wlkn0lem6  41018  21wlkdlem10  41142  11wlkdlem4  41307  31wlkdlem6  41332  31wlkdlem10  41336  eupth2lem3lem4  41399  frcond1  41438  frgr1v  41441  nfrgr2v  41442  frgr3vlem1  41443  frgr3vlem2  41444  frgr3v  41445  4cycl2vnunb-av  41460  n4cyclfrgr  41461  dfrngc2  41764  setrecseq  42231  setrec1lem4  42236  setrec2fun  42238