Theorem sseq2d 4016

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  sseq12d  4017  sseqtrd  4020  sbcrel  5790  funimass2  6649  fnssresb  6690  fnimaeq0  6701  foimacnv  6865  fvelimab  6981  ssimaexg  6995  ralima  7257  knatar  7377  frecseq123  8307  frrlem4  8314  wfrdmclOLD  8357  wfrlem12OLD  8360  onfununi  8381  oaordi  8584  oawordeulem  8592  oaass  8599  odi  8617  omass  8618  oen0  8624  oelim2  8633  nnaordi  8656  nnawordex  8675  naddunif  8731  pssnn  9208  fissuni  9397  dffi3  9471  cantnfle  9711  cantnflem1  9729  trcl  9768  r1sdom  9814  iscard2  10016  alephordi  10114  alephgeom  10122  cardaleph  10129  cardalephex  10130  ackbij2lem4  10281  cflm  10290  cfslbn  10307  cofsmo  10309  cfsmolem  10310  cfcoflem  10312  coftr  10313  alephsing  10316  fin23lem28  10380  fin23lem30  10382  fin23lem33  10385  fin1a2lem9  10448  axdc3lem2  10491  ttukeylem5  10553  pwfseqlem4a  10701  pwfseqlem4  10702  wunex2  10778  inar1  10815  sstskm  10882  fsuppmapnn0fiubex  14033  swrdnd  14692  swrd0  14696  repswswrd  14822  rtrclreclem1  15096  rtrclreclem2  15098  summolem2  15752  summo  15753  zsum  15754  sumz  15758  sumss  15760  fsumcvg3  15765  prodmolem2  15971  prodmo  15972  zprod  15973  prod1  15980  vdwlem1  17019  vdwlem12  17030  vdwlem13  17031  ramub2  17052  rami  17053  ramz2  17062  setsstruct2  17211  prdsval  17500  pwsle  17537  mrcuni  17664  gsumpropd  18691  gsumpropd2lem  18692  gsumress  18695  eqgfval  19194  sscntz  19344  resscntz  19351  lsmlub  19682  efgrelexlemb  19768  efgcpbllemb  19773  gsumval3a  19921  gsumzaddlem  19939  gsumzoppg  19962  dmdprd  20018  dprdcntz  20028  subgdmdprd  20054  subrngpropd  20568  subrgpropd  20608  islss  20932  lsslss  20959  lsspropd  21016  lsmelpr  21090  lbspropd  21098  lsslinds  21851  ltbval  22061  opsrval  22064  mhpval  22143  isbasisg  22954  tgval  22962  tgss3  22993  restbas  23166  tgrest  23167  restcld  23180  restopn2  23185  restntr  23190  cnpnei  23272  cncls2  23281  perfcls  23373  cmpsublem  23407  cmpsub  23408  cmpcld  23410  uncmp  23411  hauscmplem  23414  cmpfi  23416  nconnsubb  23431  clsconn  23438  hausllycmp  23502  1stckgenlem  23561  txbas  23575  ptbasfi  23589  txcnpi  23616  ptcnp  23630  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  qtopcld  23721  fbasssin  23844  fbssint  23846  fbun  23848  fbasrn  23892  filufint  23928  ufinffr  23937  ufildr  23939  ustval  24211  trust  24238  elmopn  24452  neibl  24514  cfilucfil  24572  icccmplem1  24844  icccmplem2  24845  bndth  24990  isphtpc  25026  metcld  25340  bcthlem1  25358  bcth  25363  ovolfioo  25502  ovolficc  25503  elovolmr  25511  ovoliunlem3  25539  ovolicc2  25557  volsuplem  25590  dyadmax  25633  dyadmbllem  25634  dyadmbl  25635  precsexlem6  28236  precsexlem7  28237  incistruhgr  29096  edgssv2  29215  wksfval  29627  2wlkdlem9  29954  3wlkdlem9  30187  sspval  30742  ubth  30892  orthin  31465  chssoc  31515  chsscon3  31519  chsscon1  31520  h1datom  31601  pjoml6i  31608  osum  31664  spansncv  31672  pjcjt2  31711  pjopyth  31739  hstel2  32238  hstle  32249  stj  32254  dmdbr5  32327  mdslmd1lem1  32344  atord  32407  chirredlem4  32412  atcvat4i  32416  mdsymlem2  32423  mdsymlem3  32424  mdsymlem8  32429  padct  32731  ssnnssfz  32789  pwrssmgc  32990  lindspropd  33411  idlsrgval  33531  constr01  33783  constrmon  33785  constrextdg2lem  33789  constrextdg2  33790  tpr2rico  33911  ordtrestNEW  33920  sigaval  34112  issiga  34113  issgon  34124  oms0  34299  omssubadd  34302  subgrwlk  35137  umgr2cycllem  35145  kur14  35221  cvmliftlem15  35303  satfsschain  35369  mclsrcl  35566  mclsval  35568  ivthALT  36336  isfne  36340  topfne  36355  neibastop3  36363  tailfb  36378  filnetlem1  36379  filnetlem4  36382  relowlssretop  37364  rdgssun  37379  poimirlem24  37651  mblfinlem2  37665  sstotbnd2  37781  sstotbnd  37782  sstotbnd3  37783  ssbnd  37795  cntotbnd  37803  cnpwstotbnd  37804  ismtyres  37815  heibor1lem  37816  heiborlem1  37818  heiborlem6  37823  heiborlem8  37825  exidreslem  37884  scottexf  38175  scott0f  38176  cnvref4  38351  dfrefrels2  38514  dfrefrel2  38516  lshpcmp  38989  lsmsat  39009  lsmsatcv  39011  lfl1dim  39122  lfl1dim2N  39123  lkrss2N  39170  psubspset  39746  paddss  39847  psubclsetN  39938  dilfsetN  40154  dilsetN  40155  diaglbN  41057  dibglbN  41168  dihlspsnat  41335  dihglb2  41344  dochffval  41351  dochfval  41352  dochvalr  41359  dochord2N  41373  dochsncom  41384  dihjat1lem  41430  dvh4dimat  41440  dvh3dimatN  41441  dvh2dimatN  41442  dochexmidlem1  41462  lpolsetN  41484  lpolconN  41489  hdmaplkr  41915  hdmapoc  41933  hlhillcs  41964  ismrc  42712  incssnn0  42722  nacsfix  42723  hbt  43142  oacl2g  43343  omcl2  43346  ofoaf  43368  naddwordnexlem4  43414  ss2iundf  43672  clsk1indlem1  44058  clsk1independent  44059  isotone1  44061  isotone2  44062  ntrclsiso  44080  ntrclsk2  44081  scottelrankd  44266  ssinc  45092  uzfissfz  45337  stoweidlem50  46065  stoweidlem57  46072  fourierdlem20  46142  fourierdlem50  46171  fourierdlem64  46185  fourierdlem86  46207  fourierdlem103  46224  fourierdlem104  46225  ovnval  46556  hoicvrrex  46571  ovnlecvr  46573  ovncvrrp  46579  ovnsubaddlem1  46585  hoidmvlelem3  46612  hoidmvle  46615  ovnhoilem1  46616  ovnhoi  46618  ovnlecvr2  46625  ovncvr2  46626  hspmbl  46644  ovolval4lem2  46665  ovolval5lem2  46668  ovolval5lem3  46669  ovolval5  46670  ovnovollem1  46671  ovnovollem2  46672  sprsymrelfvlem  47477  grlimgrtri  47963  grilcbri2  47971  uspgrsprf  48062  uspgrsprfo  48064  ssnn0ssfz  48265  lincfsuppcl  48330  lubeldm2d  48855  glbeldm2d  48856