Theorem sseq2d 4001

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  sseq12d  4002  sseqtrd  4009  sbcrel  5657  funimass2  6439  fnco  6467  fnssresb  6471  fnimaeq0  6483  foimacnv  6634  fvelimab  6739  ssimaexg  6751  knatar  7112  wfrdmcl  7965  wfrlem12  7968  onfununi  7980  oaordi  8174  oawordeulem  8182  oaass  8189  odi  8207  omass  8208  oen0  8214  oelim2  8223  nnaordi  8246  nnawordex  8265  pssnn  8738  fissuni  8831  dffi3  8897  cantnfle  9136  cantnflem1  9154  trcl  9172  r1sdom  9205  iscard2  9407  alephordi  9502  alephgeom  9510  cardaleph  9517  cardalephex  9518  ackbij2lem4  9666  cflm  9674  cfslbn  9691  cofsmo  9693  cfsmolem  9694  cfcoflem  9696  coftr  9697  alephsing  9700  fin23lem28  9764  fin23lem30  9766  fin23lem33  9769  fin1a2lem9  9832  axdc3lem2  9875  ttukeylem5  9937  fpwwe2lem5  10058  pwfseqlem4a  10085  pwfseqlem4  10086  wunex2  10162  inar1  10199  sstskm  10266  fsuppmapnn0fiubex  13363  swrdnd  14018  swrd0  14022  repswswrd  14148  rtrclreclem1  14419  rtrclreclem2  14420  summolem2  15075  summo  15076  zsum  15077  sumz  15081  sumss  15083  fsumcvg3  15088  prodmolem2  15291  prodmo  15292  zprod  15293  prod1  15300  vdwlem1  16319  vdwlem12  16330  vdwlem13  16331  ramub2  16352  rami  16353  ramz2  16362  setsstruct2  16523  prdsval  16730  pwsle  16767  mrcuni  16894  gsumpropd  17890  gsumpropd2lem  17891  gsumress  17894  eqgfval  18330  sscntz  18458  resscntz  18464  lsmlub  18792  efgrelexlemb  18878  efgcpbllemb  18883  gsumval3a  19025  gsumzaddlem  19043  gsumzoppg  19066  dmdprd  19122  dprdcntz  19132  subgdmdprd  19158  subrgpropd  19572  islss  19708  lsslss  19735  lsspropd  19791  lsmelpr  19865  lbspropd  19873  ltbval  20254  opsrval  20257  mhpval  20335  lsslinds  20977  isbasisg  21557  tgval  21565  tgss3  21596  restbas  21768  tgrest  21769  restcld  21782  restopn2  21787  restntr  21792  cnpnei  21874  cncls2  21883  perfcls  21975  cmpsublem  22009  cmpsub  22010  cmpcld  22012  uncmp  22013  hauscmplem  22016  cmpfi  22018  nconnsubb  22033  clsconn  22040  hausllycmp  22104  1stckgenlem  22163  txbas  22177  ptbasfi  22191  txcnpi  22218  ptcnp  22232  txcmplem1  22251  txcmplem2  22252  xkococnlem  22269  qtopcld  22323  fbasssin  22446  fbssint  22448  fbun  22450  fbasrn  22494  filufint  22530  ufinffr  22539  ufildr  22541  ustval  22813  trust  22840  elmopn  23054  neibl  23113  cfilucfil  23171  icccmplem1  23432  icccmplem2  23433  bndth  23564  isphtpc  23600  metcld  23911  bcthlem1  23929  bcth  23934  ovolfioo  24070  ovolficc  24071  elovolmr  24079  ovoliunlem3  24107  ovolicc2  24125  volsuplem  24158  dyadmax  24201  dyadmbllem  24202  dyadmbl  24203  incistruhgr  26866  edgssv2  26982  wksfval  27393  2wlkdlem9  27715  3wlkdlem9  27949  sspval  28502  ubth  28652  orthin  29225  chssoc  29275  chsscon3  29279  chsscon1  29280  h1datom  29361  pjoml6i  29368  osum  29424  spansncv  29432  pjcjt2  29471  pjopyth  29499  hstel2  29998  hstle  30009  stj  30014  dmdbr5  30087  mdslmd1lem1  30104  atord  30167  chirredlem4  30172  atcvat4i  30176  mdsymlem2  30183  mdsymlem3  30184  mdsymlem8  30189  padct  30457  ssnnssfz  30512  lindspropd  30945  tpr2rico  31157  ordtrestNEW  31166  sigaval  31372  issiga  31373  issgon  31384  oms0  31557  omssubadd  31560  subgrwlk  32381  umgr2cycllem  32389  kur14  32465  cvmliftlem15  32547  satfsschain  32613  mclsrcl  32810  mclsval  32812  trpredtr  33071  dftrpred3g  33074  frecseq123  33121  frrlem4  33128  ivthALT  33685  isfne  33689  topfne  33704  neibastop3  33712  tailfb  33727  filnetlem1  33728  filnetlem4  33731  csbwrecsg  34610  relowlssretop  34646  rdgssun  34661  poimirlem24  34918  mblfinlem2  34932  sstotbnd2  35054  sstotbnd  35055  sstotbnd3  35056  ssbnd  35068  cntotbnd  35076  cnpwstotbnd  35077  ismtyres  35088  heibor1lem  35089  heiborlem1  35091  heiborlem6  35096  heiborlem8  35098  exidreslem  35157  scottexf  35448  scott0f  35449  dfrefrels2  35755  dfrefrel2  35757  lshpcmp  36126  lsmsat  36146  lsmsatcv  36148  lfl1dim  36259  lfl1dim2N  36260  lkrss2N  36307  psubspset  36882  paddss  36983  psubclsetN  37074  dilfsetN  37290  dilsetN  37291  diaglbN  38193  dibglbN  38304  dihlspsnat  38471  dihglb2  38480  dochffval  38487  dochfval  38488  dochvalr  38495  dochord2N  38509  dochsncom  38520  dihjat1lem  38566  dvh4dimat  38576  dvh3dimatN  38577  dvh2dimatN  38578  dochexmidlem1  38598  lpolsetN  38620  lpolconN  38625  hdmaplkr  39051  hdmapoc  39069  hlhillcs  39096  ismrc  39305  incssnn0  39315  nacsfix  39316  hbt  39737  ss2iundf  40011  clsk1indlem1  40402  clsk1independent  40403  isotone1  40405  isotone2  40406  ntrclsiso  40424  ntrclsk2  40425  scottelrankd  40590  ssinc  41360  uzfissfz  41601  stoweidlem50  42342  stoweidlem57  42349  fourierdlem20  42419  fourierdlem50  42448  fourierdlem64  42462  fourierdlem86  42484  fourierdlem103  42501  fourierdlem104  42502  ovnval  42830  hoicvrrex  42845  ovnlecvr  42847  ovncvrrp  42853  ovnsubaddlem1  42859  hoidmvlelem3  42886  hoidmvle  42889  ovnhoilem1  42890  ovnhoi  42892  ovnlecvr2  42899  ovncvr2  42900  hspmbl  42918  ovolval4lem2  42939  ovolval5lem2  42942  ovolval5lem3  42943  ovolval5  42944  ovnovollem1  42945  ovnovollem2  42946  sprsymrelfvlem  43659  uspgrsprf  44028  uspgrsprfo  44030  ssnn0ssfz  44404  lincfsuppcl  44475