Theorem sseq1d 3946

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sseq12d  3948  eqsstrd  3953  ssiun2s  4935  disjxiun  5027  treq  5142  iunopeqop  5376  preddowncl  6143  funimass1  6406  feq1  6468  fvmptss  6757  fvimacnvi  6799  fvimacnvALT  6804  knatar  7089  ovmptss  7771  fnsuppres  7840  imacosuppOLD  7858  wrecseq123  7931  wfrlem1  7937  wfrlem3  7939  wfrdmcl  7946  wfrlem15  7952  wfrlem17  7954  dfrecs3  7992  oaordi  8155  oaword2  8162  oawordeulem  8163  omword1  8182  oewordri  8201  oeordsuc  8203  nnaordi  8227  nnawordex  8246  ereq1  8279  elpm2r  8407  inficl  8873  fipwss  8877  dffi3  8879  hartogslem1  8990  inf3lema  9071  inf3lemd  9074  cantnfle  9118  cantnflem2  9137  trcl  9154  tcmin  9167  rankr1ai  9211  rankxplim  9292  scottex  9298  scott0  9299  scottexs  9300  scott0s  9301  karden  9308  cardne  9378  cardaleph  9500  ackbij2  9654  cflim2  9674  cfslb  9677  coftr  9684  fin23lem15  9745  fin23lem32  9755  fin23lem34  9757  fin23lem35  9758  fin23lem36  9759  fin23lem41  9763  isf32lem1  9764  itunitc1  9831  axdc3lem2  9862  ttukeylem1  9920  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwe2  10054  fpwwecbv  10055  fpwwelem  10056  canthwelem  10061  canthwe  10062  wunex2  10149  wuncval2  10158  eltsk2g  10162  tskpwss  10163  inar1  10186  grothpw  10237  grothpwex  10238  axgroth6  10239  grothac  10241  peano5uzti  12060  fsuppmapnn0fiub0  13356  relexpnndm  14392  rtrclreclem4  14412  dfrtrcl2  14413  lo1o1  14881  o1lo1  14886  o1lo12  14887  lo1eq  14917  rlimeq  14918  isercoll  15016  prmreclem4  16245  vdwmc  16304  vdwlem1  16307  vdwlem2  16308  vdwlem12  16318  vdwlem13  16319  ramval  16334  ramz2  16350  ramub1lem1  16352  isacs2  16916  isacs1i  16920  mreacs  16921  acsfn  16922  rescabs  17095  ipole  17760  ipodrsima  17767  isacs5  17774  symgsssg  18587  psgnunilem5  18614  sylow1  18720  efgval2  18842  efgsfo  18857  frgpuplem  18890  gsumzf1o  19025  gsumzoppg  19057  dprdcntz  19123  islbs2  19919  frlmssuvc1  20483  frlmssuvc2  20484  frlmsslsp  20485  ismhp  20793  pptbas  21613  pnfnei  21825  mnfnei  21826  iscnp  21842  iscnp4  21868  cnntr  21880  cnconst2  21888  cnpresti  21893  cnprest  21894  isreg  21937  isnrm  21940  isnrm2  21963  perfcls  21970  isreg2  21982  hauscmplem  22011  1stcfb  22050  1stcelcls  22066  1stccnp  22067  txbas  22172  ptbasfi  22186  xkoopn  22194  xkoccn  22224  txcnp  22225  ptcnplem  22226  txdis  22237  txdis1cn  22240  txtube  22245  txkgen  22257  xkohaus  22258  xkoptsub  22259  xkoco1cn  22262  xkoco2cn  22263  xkococnlem  22264  xkococn  22265  xkoinjcn  22292  kqreglem1  22346  kqreglem2  22347  kqnrmlem1  22348  kqnrmlem2  22349  reghmph  22398  nrmhmph  22399  trfil2  22492  ufileu  22524  elfm  22552  elfm2  22553  elfm3  22555  imaelfm  22556  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  fmco  22566  elflim2  22569  flffbas  22600  lmflf  22610  txflf  22611  fclscf  22630  flimfnfcls  22633  cnextcn  22672  symgtgp  22711  ghmcnp  22720  qustgplem  22726  eltsms  22738  ustval  22808  ust0  22825  trust  22835  utoptop  22840  restutop  22843  restutopopn  22844  utopsnneiplem  22853  ucncn  22891  fmucnd  22898  cfilufg  22899  trcfilu  22900  neipcfilu  22902  blssps  23031  blss  23032  ssblex  23035  blin2  23036  metss2  23119  metrest  23131  metcnp3  23147  metustexhalf  23163  metustbl  23173  psmetutop  23174  xrsmopn  23417  recld2  23419  icccmplem1  23427  icccmplem2  23428  icccmp  23430  reconnlem2  23432  lebnumlem3  23568  lebnum  23569  xlebnum  23570  lebnumii  23571  nmhmcn  23725  cfilfval  23868  caubl  23912  caublcls  23913  bcthlem1  23928  bcth  23933  ovolfiniun  24105  ovoliunlem3  24108  ovoliun  24109  ovoliun2  24110  ovoliunnul  24111  voliunlem3  24156  dyadmax  24202  dyadmbllem  24203  dyadmbl  24204  opnmbllem  24205  ellimc2  24480  limcnlp  24481  ellimc3  24482  limcflf  24484  limciun  24497  cpnord  24538  lhop  24619  xrlimcnp  25554  cvxcl  25570  dchrval  25818  ausgrumgri  26960  ausgrusgri  26961  nbgrval  27126  nbgrel  27130  nbumgrvtx  27136  nbgrnself  27149  uvtxel1  27186  wlkonl1iedg  27455  crctcshwlkn0lem6  27601  2wlkdlem10  27721  1wlkdlem4  27925  3wlkdlem6  27950  3wlkdlem10  27954  eupth2lem3lem4  28016  frcond1  28051  frgr1v  28056  nfrgr2v  28057  frgr3vlem1  28058  frgr3vlem2  28059  frgr3v  28060  4cycl2vnunb  28075  n4cyclfrgr  28076  isssp  28507  ubthlem1  28653  shmodi  29173  chsupid  29195  chsscon3  29283  spansncvi  29435  mdslmd1lem3  30110  mdslmd1lem4  30111  mdsymlem5  30190  dmdbr5ati  30205  dmdbr6ati  30206  dmdbr7ati  30207  ssiun2sf  30323  fpwrelmapffslem  30494  pwrssmgc  30706  txomap  31187  locfinreflem  31193  tpr2rico  31265  pnfneige0  31304  rrhre  31372  prodindf  31392  dya2icoseg2  31646  omsfval  31662  eulerpartlemt0  31737  eulerpartgbij  31740  eulerpartlemr  31742  eulerpartlemgs2  31748  eulerpartlemn  31749  eulerpart  31750  bnj517  32267  bnj1014  32343  bnj1015  32344  bnj1123  32368  bnj1125  32374  bnj1450  32432  bnj1452  32434  cplgredgex  32480  kur14  32576  cvmliftlem15  32658  cvmlift2lem12  32674  cvmlift2lem13  32675  mclsval  32923  mclsax  32929  mclsppslem  32943  dfpo2  33104  trpredlem1  33179  trpredmintr  33183  frecseq123  33232  frrlem1  33236  frrlem3  33238  frrlem4  33239  frrlem13  33248  noetalem5  33334  opnrebl  33781  opnrebl2  33782  ivthALT  33796  neibastop2lem  33821  fnemeet1  33827  filnetlem1  33839  filnetlem4  33842  bj-imdirval3  34599  bj-imdiridlem  34600  csbwrecsg  34744  rdgssun  34795  lindsadd  35050  lindsenlbs  35052  ptrecube  35057  poimirlem32  35089  opnmbllem0  35093  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  ovoliunnfl  35099  ex-ovoliunnfl  35100  voliunnfl  35101  totbndbnd  35227  heibor1lem  35247  heiborlem10  35258  scottexf  35606  scott0f  35607  relcnveq2  35740  elrelscnveq2  35893  dfcnvrefrels2  35926  dfcnvrefrel2  35928  symrefref2  35959  lcv1  36337  lfl1dim  36417  lfl1dim2N  36418  paddasslem17  37132  dihglblem6  38636  dochvalr  38653  dochord3  38668  lpolconN  38783  lcfls1lem  38830  mapdffval  38922  mapdfval  38923  mapdsn2  38938  mapd0  38961  lspindp5  39066  mapdh8ab  39073  ismrcd1  39639  nacsfix  39653  setindtr  39965  hbtlem6  40073  clcnvlem  40323  iunrelexpmin1  40409  iunrelexpmin2  40413  relexp0a  40417  cotrcltrcl  40426  trclimalb2  40427  cotrclrcl  40443  sbcheg  40480  clsk1indlem1  40748  isotone1  40751  isotone2  40752  ntrclsiso  40770  ntrclsk2  40771  k0004lem1  40850  k0004lem3  40852  scottelrankd  40955  mnuop123d  40970  mnuprdlem1  40980  mnuprdlem2  40981  mnuunid  40985  mnurndlem1  40989  ssdec  41724  iinssd  41766  iinssdf  41776  ssnnf1octb  41822  iooiinicc  42179  iooiinioc  42193  icccncfext  42529  fourierdlem41  42790  meaiininclem  43125  hoidmvlelem3  43236  hoidmvle  43239  opnvonmbllem1  43271  opnvonmbl  43273  iinhoiicclem  43312  smflim  43410  smflimsuplem7  43457  uspgrsprf  44374  setrecseq  45215  setrec1lem4  45220  setrec2fun  45222