Theorem sseq1d 4014

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseq12d  4016  eqsstrd  4021  ssiun2s  5052  disjxiun  5146  treq  5274  iunopeqop  5522  dfpo2  6296  preddowncl  6334  funimass1  6631  feq1  6699  focofo  6819  fvmptss  7011  fvimacnvi  7054  fvimacnvALT  7059  knatar  7354  ovmptss  8079  fnsuppres  8176  frecseq123  8267  csbfrecsg  8269  frrlem1  8271  frrlem3  8273  frrlem4  8274  frrlem13  8283  frrdmcl  8293  fprresex  8295  wrecseq123OLD  8300  wfrlem1OLD  8308  wfrlem3OLD  8310  wfrdmclOLD  8317  wfrlem15OLD  8323  wfrlem17OLD  8325  dfrecs3  8372  dfrecs3OLD  8373  oaordi  8546  oaword2  8553  oawordeulem  8554  omword1  8573  oewordri  8592  oeordsuc  8594  nnaordi  8618  nnawordex  8637  naddcllem  8675  naddunif  8692  ereq1  8710  elpm2r  8839  inficl  9420  fipwss  9424  dffi3  9426  hartogslem1  9537  inf3lema  9619  inf3lemd  9622  cantnfle  9666  cantnflem2  9685  ttrclselem1  9720  trcl  9723  tcmin  9736  rankr1ai  9793  rankxplim  9874  scottex  9880  scott0  9881  scottexs  9882  scott0s  9883  karden  9890  cardne  9960  cardaleph  10084  ackbij2  10238  cflim2  10258  cfslb  10261  coftr  10268  fin23lem15  10329  fin23lem32  10339  fin23lem34  10341  fin23lem35  10342  fin23lem36  10343  fin23lem41  10347  isf32lem1  10348  itunitc1  10415  axdc3lem2  10446  ttukeylem1  10504  fpwwe2cbv  10625  fpwwe2lem2  10627  fpwwe2  10638  fpwwecbv  10639  fpwwelem  10640  canthwelem  10645  canthwe  10646  wunex2  10733  wuncval2  10742  eltsk2g  10746  tskpwss  10747  inar1  10770  grothpw  10821  grothpwex  10822  axgroth6  10823  grothac  10825  peano5uzti  12652  fsuppmapnn0fiub0  13958  relexpnndm  14988  rtrclreclem4  15008  dfrtrcl2  15009  lo1o1  15476  o1lo1  15481  o1lo12  15482  lo1eq  15512  rlimeq  15513  isercoll  15614  prmreclem4  16852  vdwmc  16911  vdwlem1  16914  vdwlem2  16915  vdwlem12  16925  vdwlem13  16926  ramval  16941  ramz2  16957  ramub1lem1  16959  isacs2  17597  isacs1i  17601  mreacs  17602  acsfn  17603  rescabs  17782  rescabsOLD  17783  ipole  18487  ipodrsima  18494  isacs5  18501  symgsssg  19335  psgnunilem5  19362  sylow1  19471  efgval2  19592  efgsfo  19607  frgpuplem  19640  gsumzf1o  19780  gsumzoppg  19812  dprdcntz  19878  islbs2  20767  frlmssuvc1  21349  frlmssuvc2  21350  frlmsslsp  21351  ismhp  21684  pptbas  22511  pnfnei  22724  mnfnei  22725  iscnp  22741  iscnp4  22767  cnntr  22779  cnconst2  22787  cnpresti  22792  cnprest  22793  isreg  22836  isnrm  22839  isnrm2  22862  perfcls  22869  isreg2  22881  hauscmplem  22910  1stcfb  22949  1stcelcls  22965  1stccnp  22966  txbas  23071  ptbasfi  23085  xkoopn  23093  xkoccn  23123  txcnp  23124  ptcnplem  23125  txdis  23136  txdis1cn  23139  txtube  23144  txkgen  23156  xkohaus  23157  xkoptsub  23158  xkoco1cn  23161  xkoco2cn  23162  xkococnlem  23163  xkococn  23164  xkoinjcn  23191  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  reghmph  23297  nrmhmph  23298  trfil2  23391  ufileu  23423  elfm  23451  elfm2  23452  elfm3  23454  imaelfm  23455  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  fmco  23465  elflim2  23468  flffbas  23499  lmflf  23509  txflf  23510  fclscf  23529  flimfnfcls  23532  cnextcn  23571  symgtgp  23610  ghmcnp  23619  qustgplem  23625  eltsms  23637  ustval  23707  ust0  23724  trust  23734  utoptop  23739  restutop  23742  restutopopn  23743  utopsnneiplem  23752  ucncn  23790  fmucnd  23797  cfilufg  23798  trcfilu  23799  neipcfilu  23801  blssps  23930  blss  23931  ssblex  23934  blin2  23935  metss2  24021  metrest  24033  metcnp3  24049  metustexhalf  24065  metustbl  24075  psmetutop  24076  xrsmopn  24328  recld2  24330  icccmplem1  24338  icccmplem2  24339  icccmp  24341  reconnlem2  24343  lebnumlem3  24479  lebnum  24480  xlebnum  24481  lebnumii  24482  nmhmcn  24636  cfilfval  24781  caubl  24825  caublcls  24826  bcthlem1  24841  bcth  24846  ovolfiniun  25018  ovoliunlem3  25021  ovoliun  25022  ovoliun2  25023  ovoliunnul  25024  voliunlem3  25069  dyadmax  25115  dyadmbllem  25116  dyadmbl  25117  opnmbllem  25118  ellimc2  25394  limcnlp  25395  ellimc3  25396  limcflf  25398  limciun  25411  cpnord  25452  lhop  25533  xrlimcnp  26473  cvxcl  26489  dchrval  26737  noetalem2  27245  madebdayim  27383  madebdaylemold  27393  madebday  27395  precsexlem8  27663  ausgrumgri  28458  ausgrusgri  28459  nbgrval  28624  nbgrel  28628  nbumgrvtx  28634  nbgrnself  28647  uvtxel1  28684  wlkonl1iedg  28953  crctcshwlkn0lem6  29100  2wlkdlem10  29220  1wlkdlem4  29424  3wlkdlem6  29449  3wlkdlem10  29453  eupth2lem3lem4  29515  frcond1  29550  frgr1v  29555  nfrgr2v  29556  frgr3vlem1  29557  frgr3vlem2  29558  frgr3v  29559  4cycl2vnunb  29574  n4cyclfrgr  29575  isssp  30008  ubthlem1  30154  shmodi  30674  chsupid  30696  chsscon3  30784  spansncvi  30936  mdslmd1lem3  31611  mdslmd1lem4  31612  mdsymlem5  31691  dmdbr5ati  31706  dmdbr6ati  31707  dmdbr7ati  31708  ssiun2sf  31822  fpwrelmapffslem  31988  pwrssmgc  32201  fldgenval  32433  txomap  32845  locfinreflem  32851  tpr2rico  32923  pnfneige0  32962  rrhre  33032  prodindf  33052  dya2icoseg2  33308  omsfval  33324  eulerpartlemt0  33399  eulerpartgbij  33402  eulerpartlemr  33404  eulerpartlemgs2  33410  eulerpartlemn  33411  eulerpart  33412  bnj517  33927  bnj1014  34003  bnj1015  34004  bnj1123  34028  bnj1125  34034  bnj1450  34092  bnj1452  34094  cplgredgex  34142  kur14  34238  cvmliftlem15  34320  cvmlift2lem12  34336  cvmlift2lem13  34337  mclsval  34585  mclsax  34591  mclsppslem  34605  opnrebl  35253  opnrebl2  35254  ivthALT  35268  neibastop2lem  35293  fnemeet1  35299  filnetlem1  35311  filnetlem4  35314  bj-imdirval3  36113  bj-imdiridlem  36114  rdgssun  36307  lindsadd  36529  lindsenlbs  36531  ptrecube  36536  poimirlem32  36568  opnmbllem0  36572  mblfinlem1  36573  mblfinlem2  36574  mblfinlem3  36575  ovoliunnfl  36578  ex-ovoliunnfl  36579  voliunnfl  36580  totbndbnd  36705  heibor1lem  36725  heiborlem10  36736  scottexf  37084  scott0f  37085  relcnveq2  37240  cnvref4  37267  elrelscnveq2  37411  dfcnvrefrels2  37446  dfcnvrefrel2  37448  symrefref2  37481  lcv1  37959  lfl1dim  38039  lfl1dim2N  38040  paddasslem17  38755  dihglblem6  40259  dochvalr  40276  dochord3  40291  lpolconN  40406  lcfls1lem  40453  mapdffval  40545  mapdfval  40546  mapdsn2  40561  mapd0  40584  lspindp5  40689  mapdh8ab  40696  ismrcd1  41484  nacsfix  41498  setindtr  41811  hbtlem6  41919  oaabsb  42092  tfsconcatrnss  42148  naddwordnexlem4  42200  clcnvlem  42422  iunrelexpmin1  42507  iunrelexpmin2  42511  relexp0a  42515  cotrcltrcl  42524  trclimalb2  42525  cotrclrcl  42541  sbcheg  42578  clsk1indlem1  42844  isotone1  42847  isotone2  42848  ntrclsiso  42866  ntrclsk2  42867  k0004lem1  42946  k0004lem3  42948  scottelrankd  43054  mnuop123d  43069  mnuprdlem1  43079  mnuprdlem2  43080  mnuunid  43084  mnurndlem1  43088  ssdec  43825  iinssd  43868  iinssdf  43876  ssnnf1octb  43941  iooiinicc  44303  iooiinioc  44317  icccncfext  44651  fourierdlem41  44912  meaiininclem  45250  hoidmvlelem3  45361  hoidmvle  45364  opnvonmbllem1  45396  opnvonmbl  45398  iinhoiicclem  45437  smflim  45541  smflimsuplem7  45590  uspgrsprf  46572  iscnrm3r  47629  iscnrm3l  47632  setrecseq  47778  setrec1lem4  47783  setrec2fun  47785