Theorem sseq2d 3971

Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)

Hypothesis

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sseq2d	⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sseq2 3965	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseq12d  3972  sseqtrd  3975  sbcrel  5758  funimass2  6608  fnssresb  6647  fnimaeq0  6658  foimacnv  6828  fvelimab  6943  ssimaexg  6957  ralima  7225  knatar  7345  frecseq123  8267  frrlem4  8274  onfununi  8316  oaordi  8519  oawordeulem  8527  oaass  8534  odi  8552  omass  8553  oen0  8560  oelim2  8569  nnaordi  8592  nnawordex  8611  naddunif  8668  pssnn  9141  fissuni  9302  dffi3  9379  cantnfle  9628  cantnflem1  9646  trcl  9685  r1sdom  9734  scottelrankd  9861  iscard2  9950  alephordi  10046  alephgeom  10054  cardaleph  10061  cardalephex  10062  ackbij2lem4  10212  cflm  10221  cfslbn  10239  cofsmo  10241  cfsmolem  10242  cfcoflem  10244  coftr  10245  alephsing  10248  fin23lem28  10312  fin23lem30  10314  fin23lem33  10317  fin1a2lem9  10380  axdc3lem2  10423  ttukeylem5  10485  pwfseqlem4a  10634  pwfseqlem4  10635  wunex2  10711  inar1  10748  sstskm  10815  fsuppmapnn0fiubex  14019  swrdnd  14682  swrd0  14686  repswswrd  14811  rtrclreclem1  15084  rtrclreclem2  15086  summolem2  15757  summo  15758  zsum  15759  sumz  15763  sumss  15765  fsumcvg3  15770  prodmolem2  15979  prodmo  15980  zprod  15981  prod1  15988  vdwlem1  17031  vdwlem12  17042  vdwlem13  17043  ramub2  17064  rami  17065  ramz2  17074  setsstruct2  17224  prdsval  17498  pwsle  17536  mrcuni  17667  gsumpropd  18726  gsumpropd2lem  18727  gsumress  18730  eqgfval  19235  sscntz  19387  resscntz  19394  lsmlub  19725  efgrelexlemb  19811  efgcpbllemb  19816  gsumval3a  19964  gsumzaddlem  19982  gsumzoppg  20005  dmdprd  20061  dprdcntz  20071  subgdmdprd  20097  subrngpropd  20644  subrgpropd  20684  islss  21024  lsslss  21051  lsspropd  21107  lsmelpr  21181  lbspropd  21189  lsslinds  21941  ltbval  22154  opsrval  22157  mhpval  22262  isbasisg  23065  tgval  23073  tgss3  23104  restbas  23276  tgrest  23277  restcld  23290  restopn2  23295  restntr  23300  cnpnei  23382  cncls2  23391  perfcls  23483  cmpsublem  23517  cmpsub  23518  cmpcld  23520  uncmp  23521  hauscmplem  23524  cmpfi  23526  nconnsubb  23541  clsconn  23548  hausllycmp  23612  1stckgenlem  23671  txbas  23685  ptbasfi  23699  txcnpi  23726  ptcnp  23740  txcmplem1  23759  txcmplem2  23760  xkococnlem  23777  qtopcld  23831  fbasssin  23954  fbssint  23956  fbun  23958  fbasrn  24002  filufint  24038  ufinffr  24047  ufildr  24049  ustval  24321  trust  24347  elmopn  24560  neibl  24619  cfilucfil  24677  icccmplem1  24941  icccmplem2  24942  bndth  25078  isphtpc  25114  metcld  25426  bcthlem1  25444  bcth  25449  ovolfioo  25587  ovolficc  25588  elovolmr  25596  ovoliunlem3  25624  ovolicc2  25642  volsuplem  25675  dyadmax  25718  dyadmbllem  25719  dyadmbl  25720  precsexlem6  28363  precsexlem7  28364  bdayfinbndlem1  28618  bdayfinbndlem2  28619  lnssplng  29022  incistruhgr  29338  edgssv2  29457  wksfval  29868  2wlkdlem9  30192  3wlkdlem9  30428  sspval  30984  ubth  31134  orthin  31707  chssoc  31757  chsscon3  31761  chsscon1  31762  h1datom  31843  pjoml6i  31850  osum  31906  spansncv  31914  pjcjt2  31953  pjopyth  31981  hstel2  32480  hstle  32491  stj  32496  dmdbr5  32569  mdslmd1lem1  32586  atord  32649  chirredlem4  32654  atcvat4i  32658  mdsymlem2  32665  mdsymlem3  32666  mdsymlem8  32671  padct  32975  ssnnssfz  33044  pwrssmgc  33233  lindspropd  33612  idlsrgval  33710  constr01  34049  constrmon  34051  constrextdg2lem  34055  constrextdg2  34056  constrfiss  34058  tpr2rico  34219  ordtrestNEW  34228  sigaval  34418  issiga  34419  issgon  34430  oms0  34604  omssubadd  34607  subgrwlk  35495  umgr2cycllem  35503  kur14  35579  cvmliftlem15  35661  satfsschain  35727  mclsrcl  35924  mclsval  35926  nmulprop  36553  ivthALT  36708  isfne  36712  topfne  36727  neibastop3  36735  tailfb  36750  filnetlem1  36751  filnetlem4  36754  relowlssretop  37869  rdgssun  37884  poimirlem24  38155  mblfinlem2  38169  sstotbnd2  38285  sstotbnd  38286  sstotbnd3  38287  ssbnd  38299  cntotbnd  38307  cnpwstotbnd  38308  ismtyres  38319  heibor1lem  38320  heiborlem1  38322  heiborlem6  38327  heiborlem8  38329  exidreslem  38388  scottexf  38679  scott0f  38680  cnvref4  38861  dfrefrels2  39104  dfrefrel2  39106  lshpcmp  39624  lsmsat  39644  lsmsatcv  39646  lfl1dim  39757  lfl1dim2N  39758  lkrss2N  39805  psubspset  40380  paddss  40481  psubclsetN  40572  dilfsetN  40788  dilsetN  40789  diaglbN  41691  dibglbN  41802  dihlspsnat  41969  dihglb2  41978  dochffval  41985  dochfval  41986  dochvalr  41993  dochord2N  42007  dochsncom  42018  dihjat1lem  42064  dvh4dimat  42074  dvh3dimatN  42075  dvh2dimatN  42076  dochexmidlem1  42096  lpolsetN  42118  lpolconN  42123  hdmaplkr  42549  hdmapoc  42567  hlhillcs  42594  ismrc  43294  incssnn0  43304  nacsfix  43305  hbt  43719  oacl2g  43919  omcl2  43922  ofoaf  43944  naddwordnexlem4  43990  ss2iundf  44247  clsk1indlem1  44633  clsk1independent  44634  isotone1  44636  isotone2  44637  ntrclsiso  44655  ntrclsk2  44656  ssinc  45663  uzfissfz  45900  stoweidlem50  46622  stoweidlem57  46629  fourierdlem20  46699  fourierdlem50  46728  fourierdlem64  46742  fourierdlem86  46764  fourierdlem103  46781  fourierdlem104  46782  ovnval  47113  hoicvrrex  47128  ovnlecvr  47130  ovncvrrp  47136  ovnsubaddlem1  47142  hoidmvlelem3  47169  hoidmvle  47172  ovnhoilem1  47173  ovnhoi  47175  ovnlecvr2  47182  ovncvr2  47183  hspmbl  47201  ovolval4lem2  47222  ovolval5lem2  47225  ovolval5lem3  47226  ovolval5  47227  ovnovollem1  47228  ovnovollem2  47229  sprsymrelfvlem  48094  grlimedgclnbgr  48615  grlimgrtri  48623  grilcbri2  48631  uspgrsprf  48766  uspgrsprfo  48768  ssnn0ssfz  48980  lincfsuppcl  49044  iunlub  49450  lubeldm2d  49587  glbeldm2d  49588