Theorem sseq2d 3968

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  sseq12d  3969  sseqtrd  3972  sbcrel  5738  funimass2  6583  fnssresb  6622  fnimaeq0  6633  foimacnv  6799  fvelimab  6914  ssimaexg  6928  ralima  7193  knatar  7313  frecseq123  8234  frrlem4  8241  onfununi  8283  oaordi  8483  oawordeulem  8491  oaass  8498  odi  8516  omass  8517  oen0  8524  oelim2  8533  nnaordi  8556  nnawordex  8575  naddunif  8631  pssnn  9105  fissuni  9269  dffi3  9346  cantnfle  9592  cantnflem1  9610  trcl  9649  r1sdom  9698  iscard2  9900  alephordi  9996  alephgeom  10004  cardaleph  10011  cardalephex  10012  ackbij2lem4  10163  cflm  10172  cfslbn  10189  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  coftr  10195  alephsing  10198  fin23lem28  10262  fin23lem30  10264  fin23lem33  10267  fin1a2lem9  10330  axdc3lem2  10373  ttukeylem5  10435  pwfseqlem4a  10584  pwfseqlem4  10585  wunex2  10661  inar1  10698  sstskm  10765  fsuppmapnn0fiubex  13927  swrdnd  14590  swrd0  14594  repswswrd  14719  rtrclreclem1  14992  rtrclreclem2  14994  summolem2  15651  summo  15652  zsum  15653  sumz  15657  sumss  15659  fsumcvg3  15664  prodmolem2  15870  prodmo  15871  zprod  15872  prod1  15879  vdwlem1  16921  vdwlem12  16932  vdwlem13  16933  ramub2  16954  rami  16955  ramz2  16964  setsstruct2  17113  prdsval  17387  pwsle  17425  mrcuni  17556  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  eqgfval  19117  sscntz  19267  resscntz  19274  lsmlub  19605  efgrelexlemb  19691  efgcpbllemb  19696  gsumval3a  19844  gsumzaddlem  19862  gsumzoppg  19885  dmdprd  19941  dprdcntz  19951  subgdmdprd  19977  subrngpropd  20513  subrgpropd  20553  islss  20897  lsslss  20924  lsspropd  20981  lsmelpr  21055  lbspropd  21063  lsslinds  21798  ltbval  22010  opsrval  22013  mhpval  22094  isbasisg  22903  tgval  22911  tgss3  22942  restbas  23114  tgrest  23115  restcld  23128  restopn2  23133  restntr  23138  cnpnei  23220  cncls2  23229  perfcls  23321  cmpsublem  23355  cmpsub  23356  cmpcld  23358  uncmp  23359  hauscmplem  23362  cmpfi  23364  nconnsubb  23379  clsconn  23386  hausllycmp  23450  1stckgenlem  23509  txbas  23523  ptbasfi  23537  txcnpi  23564  ptcnp  23578  txcmplem1  23597  txcmplem2  23598  xkococnlem  23615  qtopcld  23669  fbasssin  23792  fbssint  23794  fbun  23796  fbasrn  23840  filufint  23876  ufinffr  23885  ufildr  23887  ustval  24159  trust  24185  elmopn  24398  neibl  24457  cfilucfil  24515  icccmplem1  24779  icccmplem2  24780  bndth  24925  isphtpc  24961  metcld  25274  bcthlem1  25292  bcth  25297  ovolfioo  25436  ovolficc  25437  elovolmr  25445  ovoliunlem3  25473  ovolicc2  25491  volsuplem  25524  dyadmax  25567  dyadmbllem  25568  dyadmbl  25569  precsexlem6  28220  precsexlem7  28221  bdayfinbndlem1  28475  bdayfinbndlem2  28476  incistruhgr  29164  edgssv2  29283  wksfval  29695  2wlkdlem9  30019  3wlkdlem9  30255  sspval  30810  ubth  30960  orthin  31533  chssoc  31583  chsscon3  31587  chsscon1  31588  h1datom  31669  pjoml6i  31676  osum  31732  spansncv  31740  pjcjt2  31779  pjopyth  31807  hstel2  32306  hstle  32317  stj  32322  dmdbr5  32395  mdslmd1lem1  32412  atord  32475  chirredlem4  32480  atcvat4i  32484  mdsymlem2  32491  mdsymlem3  32492  mdsymlem8  32497  padct  32807  ssnnssfz  32877  pwrssmgc  33092  lindspropd  33475  idlsrgval  33595  constr01  33919  constrmon  33921  constrextdg2lem  33925  constrextdg2  33926  constrfiss  33928  tpr2rico  34089  ordtrestNEW  34098  sigaval  34288  issiga  34289  issgon  34300  oms0  34474  omssubadd  34477  subgrwlk  35345  umgr2cycllem  35353  kur14  35429  cvmliftlem15  35511  satfsschain  35577  mclsrcl  35774  mclsval  35776  ivthALT  36548  isfne  36552  topfne  36567  neibastop3  36575  tailfb  36590  filnetlem1  36591  filnetlem4  36594  relowlssretop  37612  rdgssun  37627  poimirlem24  37889  mblfinlem2  37903  sstotbnd2  38019  sstotbnd  38020  sstotbnd3  38021  ssbnd  38033  cntotbnd  38041  cnpwstotbnd  38042  ismtyres  38053  heibor1lem  38054  heiborlem1  38056  heiborlem6  38061  heiborlem8  38063  exidreslem  38122  scottexf  38413  scott0f  38414  cnvref4  38595  dfrefrels2  38838  dfrefrel2  38840  lshpcmp  39358  lsmsat  39378  lsmsatcv  39380  lfl1dim  39491  lfl1dim2N  39492  lkrss2N  39539  psubspset  40114  paddss  40215  psubclsetN  40306  dilfsetN  40522  dilsetN  40523  diaglbN  41425  dibglbN  41536  dihlspsnat  41703  dihglb2  41712  dochffval  41719  dochfval  41720  dochvalr  41727  dochord2N  41741  dochsncom  41752  dihjat1lem  41798  dvh4dimat  41808  dvh3dimatN  41809  dvh2dimatN  41810  dochexmidlem1  41830  lpolsetN  41852  lpolconN  41857  hdmaplkr  42283  hdmapoc  42301  hlhillcs  42328  ismrc  43052  incssnn0  43062  nacsfix  43063  hbt  43481  oacl2g  43681  omcl2  43684  ofoaf  43706  naddwordnexlem4  43752  ss2iundf  44009  clsk1indlem1  44395  clsk1independent  44396  isotone1  44398  isotone2  44399  ntrclsiso  44417  ntrclsk2  44418  scottelrankd  44597  ssinc  45440  uzfissfz  45679  stoweidlem50  46402  stoweidlem57  46409  fourierdlem20  46479  fourierdlem50  46508  fourierdlem64  46522  fourierdlem86  46544  fourierdlem103  46561  fourierdlem104  46562  ovnval  46893  hoicvrrex  46908  ovnlecvr  46910  ovncvrrp  46916  ovnsubaddlem1  46922  hoidmvlelem3  46949  hoidmvle  46952  ovnhoilem1  46953  ovnhoi  46955  ovnlecvr2  46962  ovncvr2  46963  hspmbl  46981  ovolval4lem2  47002  ovolval5lem2  47005  ovolval5lem3  47006  ovolval5  47007  ovnovollem1  47008  ovnovollem2  47009  sprsymrelfvlem  47844  grlimedgclnbgr  48349  grlimgrtri  48357  grilcbri2  48365  uspgrsprf  48500  uspgrsprfo  48502  ssnn0ssfz  48703  lincfsuppcl  48767  iunlub  49174  lubeldm2d  49311  glbeldm2d  49312