Theorem sseq2d 3966

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  sseq12d  3967  sseqtrd  3970  sbcrel  5765  funimass2  6620  fnssresb  6658  fnimaeq0  6669  foimacnv  6839  fvelimab  6954  ssimaexg  6968  ralima  7240  knatar  7364  frecseq123  8285  frrlem4  8292  onfununi  8334  oaordi  8537  oawordeulem  8545  oaass  8552  odi  8570  omass  8571  oen0  8578  oelim2  8587  nnaordi  8610  nnawordex  8629  naddunif  8686  pssnn  9167  fissuni  9328  dffi3  9405  cantnfle  9654  cantnflem1  9672  trcl  9711  r1sdom  9760  scottex  9876  scottelrankd  9891  iscard2  9985  alephordi  10081  alephgeom  10089  cardaleph  10096  cardalephex  10097  ackbij2lem4  10247  cflm  10255  cfslbn  10273  cofsmo  10275  cfsmolem  10276  cfcoflem  10278  coftr  10279  alephsing  10282  fin23lem28  10346  fin23lem30  10348  fin23lem33  10351  fin1a2lem9  10414  axdc3lem2  10457  ttukeylem5  10519  pwfseqlem4a  10674  pwfseqlem4  10675  wunex2  10751  inar1  10788  sstskm  10855  fsuppmapnn0fiubex  14060  swrdnd  14728  swrd0  14732  repswswrd  14859  rtrclreclem1  15134  rtrclreclem2  15136  summolem2  15806  summo  15807  zsum  15808  sumz  15812  sumss  15814  fsumcvg3  15819  prodmolem2  16028  prodmo  16029  zprod  16030  prod1  16037  vdwlem1  17079  vdwlem12  17090  vdwlem13  17091  ramub2  17112  rami  17113  ramz2  17122  setsstruct2  17272  prdsval  17546  pwsle  17584  mrcuni  17715  gsumpropd  18786  gsumpropd2lem  18787  gsumress  18790  eqgfval  19307  sscntz  19459  resscntz  19466  lsmlub  19797  efgrelexlemb  19883  efgcpbllemb  19888  gsumval3a  20036  gsumzaddlem  20054  gsumzoppg  20077  dmdprd  20133  dprdcntz  20143  subgdmdprd  20169  subrngpropd  20736  subrgpropd  20776  islss  21124  lsslss  21151  lsspropd  21207  lsmelpr  21281  lbspropd  21289  lsslinds  22050  ltbval  22265  opsrval  22268  mhpval  22373  isbasisg  23178  tgval  23186  tgss3  23217  restbas  23389  tgrest  23390  restcld  23403  restopn2  23408  restntr  23413  cnpnei  23495  cncls2  23504  perfcls  23596  cmpsublem  23630  cmpsub  23631  cmpcld  23633  uncmp  23634  hauscmplem  23637  cmpfi  23639  nconnsubb  23654  clsconn  23661  hausllycmp  23726  1stckgenlem  23785  txbas  23799  ptbasfi  23813  txcnpi  23840  ptcnp  23854  txcmplem1  23873  txcmplem2  23874  xkococnlem  23891  qtopcld  23945  fbasssin  24068  fbssint  24070  fbun  24072  fbasrn  24116  filufint  24152  ufinffr  24161  ufildr  24163  ustval  24435  trust  24461  elmopn  24674  neibl  24733  cfilucfil  24791  icccmplem1  25055  icccmplem2  25056  bndth  25192  isphtpc  25228  metcld  25540  bcthlem1  25558  bcth  25563  ovolfioo  25701  ovolficc  25702  elovolmr  25710  ovoliunlem3  25738  ovolicc2  25756  volsuplem  25789  dyadmax  25832  dyadmbllem  25833  dyadmbl  25834  precsexlem6  28485  precsexlem7  28486  bdayfinbndlem1  28740  bdayfinbndlem2  28741  lnssplng  29157  incistruhgr  29544  edgssv2  29666  wksfval  30077  subgrwlk  30156  2wlkdlem9  30410  3wlkdlem9  30656  sspval  31212  ubth  31362  orthin  31935  chssoc  31985  chsscon3  31989  chsscon1  31990  h1datom  32071  pjoml6i  32078  osum  32134  spansncv  32142  pjcjt2  32181  pjopyth  32209  hstel2  32708  hstle  32719  stj  32724  dmdbr5  32797  mdslmd1lem1  32814  atord  32877  chirredlem4  32882  atcvat4i  32886  mdsymlem2  32893  mdsymlem3  32894  mdsymlem8  32899  padct  33197  ssnnssfz  33266  pwrssmgc  33448  lindspropd  33824  idlsrgval  33921  constr01  34260  constrmon  34262  constrextdg2lem  34266  constrextdg2  34267  constrfiss  34269  tpr2rico  34430  ordtrestNEW  34439  sigaval  34629  issiga  34630  issgon  34641  oms0  34816  omssubadd  34819  elscottrankss  35638  kur14  35803  cvmliftlem15  35885  satfsschain  35951  mclsrcl  36148  mclsval  36150  nmulprop  36778  ivthALT  36962  isfne  36966  topfne  36981  neibastop3  36989  tailfb  37004  filnetlem1  37005  filnetlem4  37008  relowlssretop  38125  rdgssun  38140  poimirlem24  38401  mblfinlem2  38415  sstotbnd2  38532  sstotbnd  38533  sstotbnd3  38534  ssbnd  38546  cntotbnd  38554  cnpwstotbnd  38555  ismtyres  38566  heibor1lem  38567  heiborlem1  38569  heiborlem6  38574  heiborlem8  38576  exidreslem  38635  scottexf  38924  scott0f  38925  cnvref4  39106  dfrefrels2  39349  dfrefrel2  39351  lshpcmp  39869  lsmsat  39889  lsmsatcv  39891  lfl1dim  40002  lfl1dim2N  40003  lkrss2N  40050  psubspset  40625  paddss  40726  psubclsetN  40817  dilfsetN  41033  dilsetN  41034  diaglbN  41936  dibglbN  42047  dihlspsnat  42214  dihglb2  42223  dochffval  42230  dochfval  42231  dochvalr  42238  dochord2N  42252  dochsncom  42263  dihjat1lem  42309  dvh4dimat  42319  dvh3dimatN  42320  dvh2dimatN  42321  dochexmidlem1  42341  lpolsetN  42363  lpolconN  42368  hdmaplkr  42794  hdmapoc  42812  hlhillcs  42839  ismrc  43554  incssnn0  43564  nacsfix  43565  hbt  43979  oacl2g  44179  omcl2  44182  ofoaf  44204  naddwordnexlem4  44250  ss2iundf  44507  clsk1indlem1  44893  clsk1independent  44894  isotone1  44896  isotone2  44897  ntrclsiso  44915  ntrclsk2  44916  ssinc  45927  uzfissfz  46164  stoweidlem50  46886  stoweidlem57  46893  fourierdlem20  46963  fourierdlem50  46992  fourierdlem64  47006  fourierdlem86  47028  fourierdlem103  47045  fourierdlem104  47046  ovnval  47377  hoicvrrex  47392  ovnlecvr  47394  ovncvrrp  47400  ovnsubaddlem1  47406  hoidmvlelem3  47433  hoidmvle  47436  ovnhoilem1  47437  ovnhoi  47439  ovnlecvr2  47446  ovncvr2  47447  hspmbl  47465  ovolval4lem2  47486  ovolval5lem2  47489  ovolval5lem3  47490  ovolval5  47491  ovnovollem1  47492  ovnovollem2  47493  sprsymrelfvlem  48398  grlimedgclnbgr  48919  grlimgrtri  48927  grilcbri2  48935  uspgrsprf  49070  uspgrsprfo  49072  ssnn0ssfz  49287  lincfsuppcl  49351  iunlub  49757  lubeldm2d  49892  glbeldm2d  49893