Theorem sseq1d 4013

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  sseq12d  4015  eqsstrd  4020  ssiun2s  5051  disjxiun  5145  treq  5273  iunopeqop  5521  dfpo2  6295  preddowncl  6333  funimass1  6630  feq1  6698  focofo  6818  fvmptss  7010  fvimacnvi  7053  fvimacnvALT  7058  knatar  7356  ovmptss  8081  fnsuppres  8178  frecseq123  8269  csbfrecsg  8271  frrlem1  8273  frrlem3  8275  frrlem4  8276  frrlem13  8285  frrdmcl  8295  fprresex  8297  wrecseq123OLD  8302  wfrlem1OLD  8310  wfrlem3OLD  8312  wfrdmclOLD  8319  wfrlem15OLD  8325  wfrlem17OLD  8327  dfrecs3  8374  dfrecs3OLD  8375  oaordi  8548  oaword2  8555  oawordeulem  8556  omword1  8575  oewordri  8594  oeordsuc  8596  nnaordi  8620  nnawordex  8639  naddcllem  8677  naddunif  8694  ereq1  8712  elpm2r  8841  inficl  9422  fipwss  9426  dffi3  9428  hartogslem1  9539  inf3lema  9621  inf3lemd  9624  cantnfle  9668  cantnflem2  9687  ttrclselem1  9722  trcl  9725  tcmin  9738  rankr1ai  9795  rankxplim  9876  scottex  9882  scott0  9883  scottexs  9884  scott0s  9885  karden  9892  cardne  9962  cardaleph  10086  ackbij2  10240  cflim2  10260  cfslb  10263  coftr  10270  fin23lem15  10331  fin23lem32  10341  fin23lem34  10343  fin23lem35  10344  fin23lem36  10345  fin23lem41  10349  isf32lem1  10350  itunitc1  10417  axdc3lem2  10448  ttukeylem1  10506  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwe2  10640  fpwwecbv  10641  fpwwelem  10642  canthwelem  10647  canthwe  10648  wunex2  10735  wuncval2  10744  eltsk2g  10748  tskpwss  10749  inar1  10772  grothpw  10823  grothpwex  10824  axgroth6  10825  grothac  10827  peano5uzti  12656  fsuppmapnn0fiub0  13962  relexpnndm  14992  rtrclreclem4  15012  dfrtrcl2  15013  lo1o1  15480  o1lo1  15485  o1lo12  15486  lo1eq  15516  rlimeq  15517  isercoll  15618  prmreclem4  16856  vdwmc  16915  vdwlem1  16918  vdwlem2  16919  vdwlem12  16929  vdwlem13  16930  ramval  16945  ramz2  16961  ramub1lem1  16963  isacs2  17601  isacs1i  17605  mreacs  17606  acsfn  17607  rescabs  17786  rescabsOLD  17787  ipole  18491  ipodrsima  18498  isacs5  18505  symgsssg  19376  psgnunilem5  19403  sylow1  19512  efgval2  19633  efgsfo  19648  frgpuplem  19681  gsumzf1o  19821  gsumzoppg  19853  dprdcntz  19919  islbs2  20912  frlmssuvc1  21568  frlmssuvc2  21569  frlmsslsp  21570  ismhp  21903  pptbas  22731  pnfnei  22944  mnfnei  22945  iscnp  22961  iscnp4  22987  cnntr  22999  cnconst2  23007  cnpresti  23012  cnprest  23013  isreg  23056  isnrm  23059  isnrm2  23082  perfcls  23089  isreg2  23101  hauscmplem  23130  1stcfb  23169  1stcelcls  23185  1stccnp  23186  txbas  23291  ptbasfi  23305  xkoopn  23313  xkoccn  23343  txcnp  23344  ptcnplem  23345  txdis  23356  txdis1cn  23359  txtube  23364  txkgen  23376  xkohaus  23377  xkoptsub  23378  xkoco1cn  23381  xkoco2cn  23382  xkococnlem  23383  xkococn  23384  xkoinjcn  23411  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  reghmph  23517  nrmhmph  23518  trfil2  23611  ufileu  23643  elfm  23671  elfm2  23672  elfm3  23674  imaelfm  23675  rnelfm  23677  fmfnfmlem2  23679  fmfnfmlem4  23681  fmco  23685  elflim2  23688  flffbas  23719  lmflf  23729  txflf  23730  fclscf  23749  flimfnfcls  23752  cnextcn  23791  symgtgp  23830  ghmcnp  23839  qustgplem  23845  eltsms  23857  ustval  23927  ust0  23944  trust  23954  utoptop  23959  restutop  23962  restutopopn  23963  utopsnneiplem  23972  ucncn  24010  fmucnd  24017  cfilufg  24018  trcfilu  24019  neipcfilu  24021  blssps  24150  blss  24151  ssblex  24154  blin2  24155  metss2  24241  metrest  24253  metcnp3  24269  metustexhalf  24285  metustbl  24295  psmetutop  24296  xrsmopn  24548  recld2  24550  icccmplem1  24558  icccmplem2  24559  icccmp  24561  reconnlem2  24563  lebnumlem3  24703  lebnum  24704  xlebnum  24705  lebnumii  24706  nmhmcn  24860  cfilfval  25005  caubl  25049  caublcls  25050  bcthlem1  25065  bcth  25070  ovolfiniun  25242  ovoliunlem3  25245  ovoliun  25246  ovoliun2  25247  ovoliunnul  25248  voliunlem3  25293  dyadmax  25339  dyadmbllem  25340  dyadmbl  25341  opnmbllem  25342  ellimc2  25618  limcnlp  25619  ellimc3  25620  limcflf  25622  limciun  25635  cpnord  25676  lhop  25757  xrlimcnp  26697  cvxcl  26713  dchrval  26961  noetalem2  27469  madebdayim  27607  madebdaylemold  27617  madebday  27619  precsexlem8  27887  ausgrumgri  28682  ausgrusgri  28683  nbgrval  28848  nbgrel  28852  nbumgrvtx  28858  nbgrnself  28871  uvtxel1  28908  wlkonl1iedg  29177  crctcshwlkn0lem6  29324  2wlkdlem10  29444  1wlkdlem4  29648  3wlkdlem6  29673  3wlkdlem10  29677  eupth2lem3lem4  29739  frcond1  29774  frgr1v  29779  nfrgr2v  29780  frgr3vlem1  29781  frgr3vlem2  29782  frgr3v  29783  4cycl2vnunb  29798  n4cyclfrgr  29799  isssp  30232  ubthlem1  30378  shmodi  30898  chsupid  30920  chsscon3  31008  spansncvi  31160  mdslmd1lem3  31835  mdslmd1lem4  31836  mdsymlem5  31915  dmdbr5ati  31930  dmdbr6ati  31931  dmdbr7ati  31932  ssiun2sf  32046  fpwrelmapffslem  32212  pwrssmgc  32425  fldgenval  32660  resssra  32950  txomap  33100  locfinreflem  33106  tpr2rico  33178  pnfneige0  33217  rrhre  33287  prodindf  33307  dya2icoseg2  33563  omsfval  33579  eulerpartlemt0  33654  eulerpartgbij  33657  eulerpartlemr  33659  eulerpartlemgs2  33665  eulerpartlemn  33666  eulerpart  33667  bnj517  34182  bnj1014  34258  bnj1015  34259  bnj1123  34283  bnj1125  34289  bnj1450  34347  bnj1452  34349  cplgredgex  34397  kur14  34493  cvmliftlem15  34575  cvmlift2lem12  34591  cvmlift2lem13  34592  mclsval  34840  mclsax  34846  mclsppslem  34860  opnrebl  35508  opnrebl2  35509  ivthALT  35523  neibastop2lem  35548  fnemeet1  35554  filnetlem1  35566  filnetlem4  35569  bj-imdirval3  36368  bj-imdiridlem  36369  rdgssun  36562  lindsadd  36784  lindsenlbs  36786  ptrecube  36791  poimirlem32  36823  opnmbllem0  36827  mblfinlem1  36828  mblfinlem2  36829  mblfinlem3  36830  ovoliunnfl  36833  ex-ovoliunnfl  36834  voliunnfl  36835  totbndbnd  36960  heibor1lem  36980  heiborlem10  36991  scottexf  37339  scott0f  37340  relcnveq2  37495  cnvref4  37522  elrelscnveq2  37666  dfcnvrefrels2  37701  dfcnvrefrel2  37703  symrefref2  37736  lcv1  38214  lfl1dim  38294  lfl1dim2N  38295  paddasslem17  39010  dihglblem6  40514  dochvalr  40531  dochord3  40546  lpolconN  40661  lcfls1lem  40708  mapdffval  40800  mapdfval  40801  mapdsn2  40816  mapd0  40839  lspindp5  40944  mapdh8ab  40951  ismrcd1  41738  nacsfix  41752  setindtr  42065  hbtlem6  42173  oaabsb  42346  tfsconcatrnss  42402  naddwordnexlem4  42454  clcnvlem  42676  iunrelexpmin1  42761  iunrelexpmin2  42765  relexp0a  42769  cotrcltrcl  42778  trclimalb2  42779  cotrclrcl  42795  sbcheg  42832  clsk1indlem1  43098  isotone1  43101  isotone2  43102  ntrclsiso  43120  ntrclsk2  43121  k0004lem1  43200  k0004lem3  43202  scottelrankd  43308  mnuop123d  43323  mnuprdlem1  43333  mnuprdlem2  43334  mnuunid  43338  mnurndlem1  43342  ssdec  44079  iinssd  44122  iinssdf  44130  ssnnf1octb  44192  iooiinicc  44554  iooiinioc  44568  icccncfext  44902  fourierdlem41  45163  meaiininclem  45501  hoidmvlelem3  45612  hoidmvle  45615  opnvonmbllem1  45647  opnvonmbl  45649  iinhoiicclem  45688  smflim  45792  smflimsuplem7  45841  uspgrsprf  46823  iscnrm3r  47669  iscnrm3l  47672  setrecseq  47818  setrec1lem4  47823  setrec2fun  47825