Theorem sseq2d 4027

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  sseq12d  4028  sseqtrd  4035  sbcrel  5792  funimass2  6650  fnssresb  6690  fnimaeq0  6701  foimacnv  6865  fvelimab  6980  ssimaexg  6994  ralima  7256  knatar  7376  frecseq123  8305  frrlem4  8312  wfrdmclOLD  8355  wfrlem12OLD  8358  onfununi  8379  oaordi  8582  oawordeulem  8590  oaass  8597  odi  8615  omass  8616  oen0  8622  oelim2  8631  nnaordi  8654  nnawordex  8673  naddunif  8729  pssnn  9206  fissuni  9394  dffi3  9468  cantnfle  9708  cantnflem1  9726  trcl  9765  r1sdom  9811  iscard2  10013  alephordi  10111  alephgeom  10119  cardaleph  10126  cardalephex  10127  ackbij2lem4  10278  cflm  10287  cfslbn  10304  cofsmo  10306  cfsmolem  10307  cfcoflem  10309  coftr  10310  alephsing  10313  fin23lem28  10377  fin23lem30  10379  fin23lem33  10382  fin1a2lem9  10445  axdc3lem2  10488  ttukeylem5  10550  pwfseqlem4a  10698  pwfseqlem4  10699  wunex2  10775  inar1  10812  sstskm  10879  fsuppmapnn0fiubex  14029  swrdnd  14688  swrd0  14692  repswswrd  14818  rtrclreclem1  15092  rtrclreclem2  15094  summolem2  15748  summo  15749  zsum  15750  sumz  15754  sumss  15756  fsumcvg3  15761  prodmolem2  15967  prodmo  15968  zprod  15969  prod1  15976  vdwlem1  17014  vdwlem12  17025  vdwlem13  17026  ramub2  17047  rami  17048  ramz2  17057  setsstruct2  17207  prdsval  17501  pwsle  17538  mrcuni  17665  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  eqgfval  19206  sscntz  19356  resscntz  19363  lsmlub  19696  efgrelexlemb  19782  efgcpbllemb  19787  gsumval3a  19935  gsumzaddlem  19953  gsumzoppg  19976  dmdprd  20032  dprdcntz  20042  subgdmdprd  20068  subrngpropd  20584  subrgpropd  20624  islss  20949  lsslss  20976  lsspropd  21033  lsmelpr  21107  lbspropd  21115  lsslinds  21868  ltbval  22078  opsrval  22081  mhpval  22160  isbasisg  22969  tgval  22977  tgss3  23008  restbas  23181  tgrest  23182  restcld  23195  restopn2  23200  restntr  23205  cnpnei  23287  cncls2  23296  perfcls  23388  cmpsublem  23422  cmpsub  23423  cmpcld  23425  uncmp  23426  hauscmplem  23429  cmpfi  23431  nconnsubb  23446  clsconn  23453  hausllycmp  23517  1stckgenlem  23576  txbas  23590  ptbasfi  23604  txcnpi  23631  ptcnp  23645  txcmplem1  23664  txcmplem2  23665  xkococnlem  23682  qtopcld  23736  fbasssin  23859  fbssint  23861  fbun  23863  fbasrn  23907  filufint  23943  ufinffr  23952  ufildr  23954  ustval  24226  trust  24253  elmopn  24467  neibl  24529  cfilucfil  24587  icccmplem1  24857  icccmplem2  24858  bndth  25003  isphtpc  25039  metcld  25353  bcthlem1  25371  bcth  25376  ovolfioo  25515  ovolficc  25516  elovolmr  25524  ovoliunlem3  25552  ovolicc2  25570  volsuplem  25603  dyadmax  25646  dyadmbllem  25647  dyadmbl  25648  precsexlem6  28250  precsexlem7  28251  incistruhgr  29110  edgssv2  29229  wksfval  29641  2wlkdlem9  29963  3wlkdlem9  30196  sspval  30751  ubth  30901  orthin  31474  chssoc  31524  chsscon3  31528  chsscon1  31529  h1datom  31610  pjoml6i  31617  osum  31673  spansncv  31681  pjcjt2  31720  pjopyth  31748  hstel2  32247  hstle  32258  stj  32263  dmdbr5  32336  mdslmd1lem1  32353  atord  32416  chirredlem4  32421  atcvat4i  32425  mdsymlem2  32432  mdsymlem3  32433  mdsymlem8  32438  padct  32736  ssnnssfz  32795  pwrssmgc  32974  lindspropd  33390  idlsrgval  33510  constr01  33746  constrmon  33748  tpr2rico  33872  ordtrestNEW  33881  sigaval  34091  issiga  34092  issgon  34103  oms0  34278  omssubadd  34281  subgrwlk  35116  umgr2cycllem  35124  kur14  35200  cvmliftlem15  35282  satfsschain  35348  mclsrcl  35545  mclsval  35547  ivthALT  36317  isfne  36321  topfne  36336  neibastop3  36344  tailfb  36359  filnetlem1  36360  filnetlem4  36363  relowlssretop  37345  rdgssun  37360  poimirlem24  37630  mblfinlem2  37644  sstotbnd2  37760  sstotbnd  37761  sstotbnd3  37762  ssbnd  37774  cntotbnd  37782  cnpwstotbnd  37783  ismtyres  37794  heibor1lem  37795  heiborlem1  37797  heiborlem6  37802  heiborlem8  37804  exidreslem  37863  scottexf  38154  scott0f  38155  cnvref4  38331  dfrefrels2  38494  dfrefrel2  38496  lshpcmp  38969  lsmsat  38989  lsmsatcv  38991  lfl1dim  39102  lfl1dim2N  39103  lkrss2N  39150  psubspset  39726  paddss  39827  psubclsetN  39918  dilfsetN  40134  dilsetN  40135  diaglbN  41037  dibglbN  41148  dihlspsnat  41315  dihglb2  41324  dochffval  41331  dochfval  41332  dochvalr  41339  dochord2N  41353  dochsncom  41364  dihjat1lem  41410  dvh4dimat  41420  dvh3dimatN  41421  dvh2dimatN  41422  dochexmidlem1  41442  lpolsetN  41464  lpolconN  41469  hdmaplkr  41895  hdmapoc  41913  hlhillcs  41944  ismrc  42688  incssnn0  42698  nacsfix  42699  hbt  43118  oacl2g  43319  omcl2  43322  ofoaf  43344  naddwordnexlem4  43390  ss2iundf  43648  clsk1indlem1  44034  clsk1independent  44035  isotone1  44037  isotone2  44038  ntrclsiso  44056  ntrclsk2  44057  scottelrankd  44242  ssinc  45026  uzfissfz  45275  stoweidlem50  46005  stoweidlem57  46012  fourierdlem20  46082  fourierdlem50  46111  fourierdlem64  46125  fourierdlem86  46147  fourierdlem103  46164  fourierdlem104  46165  ovnval  46496  hoicvrrex  46511  ovnlecvr  46513  ovncvrrp  46519  ovnsubaddlem1  46525  hoidmvlelem3  46552  hoidmvle  46555  ovnhoilem1  46556  ovnhoi  46558  ovnlecvr2  46565  ovncvr2  46566  hspmbl  46584  ovolval4lem2  46605  ovolval5lem2  46608  ovolval5lem3  46609  ovolval5  46610  ovnovollem1  46611  ovnovollem2  46612  sprsymrelfvlem  47414  grlimgrtri  47898  grilcbri2  47906  uspgrsprf  47989  uspgrsprfo  47991  ssnn0ssfz  48193  lincfsuppcl  48258  lubeldm2d  48754  glbeldm2d  48755