Theorem sseq2d 4041

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseq12d  4042  sseqtrd  4049  sbcrel  5804  funimass2  6661  fncoOLD  6698  fnssresb  6702  fnimaeq0  6713  foimacnv  6879  fvelimab  6994  ssimaexg  7008  ralima  7274  knatar  7393  frecseq123  8323  frrlem4  8330  wfrdmclOLD  8373  wfrlem12OLD  8376  onfununi  8397  oaordi  8602  oawordeulem  8610  oaass  8617  odi  8635  omass  8636  oen0  8642  oelim2  8651  nnaordi  8674  nnawordex  8693  naddunif  8749  pssnn  9234  fissuni  9427  dffi3  9500  cantnfle  9740  cantnflem1  9758  trcl  9797  r1sdom  9843  iscard2  10045  alephordi  10143  alephgeom  10151  cardaleph  10158  cardalephex  10159  ackbij2lem4  10310  cflm  10319  cfslbn  10336  cofsmo  10338  cfsmolem  10339  cfcoflem  10341  coftr  10342  alephsing  10345  fin23lem28  10409  fin23lem30  10411  fin23lem33  10414  fin1a2lem9  10477  axdc3lem2  10520  ttukeylem5  10582  pwfseqlem4a  10730  pwfseqlem4  10731  wunex2  10807  inar1  10844  sstskm  10911  fsuppmapnn0fiubex  14043  swrdnd  14702  swrd0  14706  repswswrd  14832  rtrclreclem1  15106  rtrclreclem2  15108  summolem2  15764  summo  15765  zsum  15766  sumz  15770  sumss  15772  fsumcvg3  15777  prodmolem2  15983  prodmo  15984  zprod  15985  prod1  15992  vdwlem1  17028  vdwlem12  17039  vdwlem13  17040  ramub2  17061  rami  17062  ramz2  17071  setsstruct2  17221  prdsval  17515  pwsle  17552  mrcuni  17679  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  eqgfval  19216  sscntz  19366  resscntz  19373  lsmlub  19706  efgrelexlemb  19792  efgcpbllemb  19797  gsumval3a  19945  gsumzaddlem  19963  gsumzoppg  19986  dmdprd  20042  dprdcntz  20052  subgdmdprd  20078  subrngpropd  20594  subrgpropd  20636  islss  20955  lsslss  20982  lsspropd  21039  lsmelpr  21113  lbspropd  21121  lsslinds  21874  ltbval  22084  opsrval  22087  mhpval  22166  isbasisg  22975  tgval  22983  tgss3  23014  restbas  23187  tgrest  23188  restcld  23201  restopn2  23206  restntr  23211  cnpnei  23293  cncls2  23302  perfcls  23394  cmpsublem  23428  cmpsub  23429  cmpcld  23431  uncmp  23432  hauscmplem  23435  cmpfi  23437  nconnsubb  23452  clsconn  23459  hausllycmp  23523  1stckgenlem  23582  txbas  23596  ptbasfi  23610  txcnpi  23637  ptcnp  23651  txcmplem1  23670  txcmplem2  23671  xkococnlem  23688  qtopcld  23742  fbasssin  23865  fbssint  23867  fbun  23869  fbasrn  23913  filufint  23949  ufinffr  23958  ufildr  23960  ustval  24232  trust  24259  elmopn  24473  neibl  24535  cfilucfil  24593  icccmplem1  24863  icccmplem2  24864  bndth  25009  isphtpc  25045  metcld  25359  bcthlem1  25377  bcth  25382  ovolfioo  25521  ovolficc  25522  elovolmr  25530  ovoliunlem3  25558  ovolicc2  25576  volsuplem  25609  dyadmax  25652  dyadmbllem  25653  dyadmbl  25654  precsexlem6  28254  precsexlem7  28255  incistruhgr  29114  edgssv2  29233  wksfval  29645  2wlkdlem9  29967  3wlkdlem9  30200  sspval  30755  ubth  30905  orthin  31478  chssoc  31528  chsscon3  31532  chsscon1  31533  h1datom  31614  pjoml6i  31621  osum  31677  spansncv  31685  pjcjt2  31724  pjopyth  31752  hstel2  32251  hstle  32262  stj  32267  dmdbr5  32340  mdslmd1lem1  32357  atord  32420  chirredlem4  32425  atcvat4i  32429  mdsymlem2  32436  mdsymlem3  32437  mdsymlem8  32442  padct  32733  ssnnssfz  32792  pwrssmgc  32973  lindspropd  33376  idlsrgval  33496  constr01  33732  constrmon  33734  tpr2rico  33858  ordtrestNEW  33867  sigaval  34075  issiga  34076  issgon  34087  oms0  34262  omssubadd  34265  subgrwlk  35100  umgr2cycllem  35108  kur14  35184  cvmliftlem15  35266  satfsschain  35332  mclsrcl  35529  mclsval  35531  ivthALT  36301  isfne  36305  topfne  36320  neibastop3  36328  tailfb  36343  filnetlem1  36344  filnetlem4  36347  relowlssretop  37329  rdgssun  37344  poimirlem24  37604  mblfinlem2  37618  sstotbnd2  37734  sstotbnd  37735  sstotbnd3  37736  ssbnd  37748  cntotbnd  37756  cnpwstotbnd  37757  ismtyres  37768  heibor1lem  37769  heiborlem1  37771  heiborlem6  37776  heiborlem8  37778  exidreslem  37837  scottexf  38128  scott0f  38129  cnvref4  38306  dfrefrels2  38469  dfrefrel2  38471  lshpcmp  38944  lsmsat  38964  lsmsatcv  38966  lfl1dim  39077  lfl1dim2N  39078  lkrss2N  39125  psubspset  39701  paddss  39802  psubclsetN  39893  dilfsetN  40109  dilsetN  40110  diaglbN  41012  dibglbN  41123  dihlspsnat  41290  dihglb2  41299  dochffval  41306  dochfval  41307  dochvalr  41314  dochord2N  41328  dochsncom  41339  dihjat1lem  41385  dvh4dimat  41395  dvh3dimatN  41396  dvh2dimatN  41397  dochexmidlem1  41417  lpolsetN  41439  lpolconN  41444  hdmaplkr  41870  hdmapoc  41888  hlhillcs  41919  ismrc  42657  incssnn0  42667  nacsfix  42668  hbt  43087  oacl2g  43292  omcl2  43295  ofoaf  43317  naddwordnexlem4  43363  ss2iundf  43621  clsk1indlem1  44007  clsk1independent  44008  isotone1  44010  isotone2  44011  ntrclsiso  44029  ntrclsk2  44030  scottelrankd  44216  ssinc  44989  uzfissfz  45241  stoweidlem50  45971  stoweidlem57  45978  fourierdlem20  46048  fourierdlem50  46077  fourierdlem64  46091  fourierdlem86  46113  fourierdlem103  46130  fourierdlem104  46131  ovnval  46462  hoicvrrex  46477  ovnlecvr  46479  ovncvrrp  46485  ovnsubaddlem1  46491  hoidmvlelem3  46518  hoidmvle  46521  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  ovncvr2  46532  hspmbl  46550  ovolval4lem2  46571  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovollem1  46577  ovnovollem2  46578  sprsymrelfvlem  47364  grlimgrtri  47820  grilcbri2  47828  uspgrsprf  47869  uspgrsprfo  47871  ssnn0ssfz  48074  lincfsuppcl  48142  lubeldm2d  48638  glbeldm2d  48639