Theorem sseq2d 3982

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

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

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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  sseq12d  3983  sseqtrd  3986  sbcrel  5746  funimass2  6602  fnssresb  6643  fnimaeq0  6654  foimacnv  6820  fvelimab  6936  ssimaexg  6950  ralima  7214  knatar  7335  frecseq123  8264  frrlem4  8271  onfununi  8313  oaordi  8513  oawordeulem  8521  oaass  8528  odi  8546  omass  8547  oen0  8553  oelim2  8562  nnaordi  8585  nnawordex  8604  naddunif  8660  pssnn  9138  fissuni  9315  dffi3  9389  cantnfle  9631  cantnflem1  9649  trcl  9688  r1sdom  9734  iscard2  9936  alephordi  10034  alephgeom  10042  cardaleph  10049  cardalephex  10050  ackbij2lem4  10201  cflm  10210  cfslbn  10227  cofsmo  10229  cfsmolem  10230  cfcoflem  10232  coftr  10233  alephsing  10236  fin23lem28  10300  fin23lem30  10302  fin23lem33  10305  fin1a2lem9  10368  axdc3lem2  10411  ttukeylem5  10473  pwfseqlem4a  10621  pwfseqlem4  10622  wunex2  10698  inar1  10735  sstskm  10802  fsuppmapnn0fiubex  13964  swrdnd  14626  swrd0  14630  repswswrd  14756  rtrclreclem1  15030  rtrclreclem2  15032  summolem2  15689  summo  15690  zsum  15691  sumz  15695  sumss  15697  fsumcvg3  15702  prodmolem2  15908  prodmo  15909  zprod  15910  prod1  15917  vdwlem1  16959  vdwlem12  16970  vdwlem13  16971  ramub2  16992  rami  16993  ramz2  17002  setsstruct2  17151  prdsval  17425  pwsle  17462  mrcuni  17589  gsumpropd  18612  gsumpropd2lem  18613  gsumress  18616  eqgfval  19115  sscntz  19265  resscntz  19272  lsmlub  19601  efgrelexlemb  19687  efgcpbllemb  19692  gsumval3a  19840  gsumzaddlem  19858  gsumzoppg  19881  dmdprd  19937  dprdcntz  19947  subgdmdprd  19973  subrngpropd  20484  subrgpropd  20524  islss  20847  lsslss  20874  lsspropd  20931  lsmelpr  21005  lbspropd  21013  lsslinds  21747  ltbval  21957  opsrval  21960  mhpval  22033  isbasisg  22841  tgval  22849  tgss3  22880  restbas  23052  tgrest  23053  restcld  23066  restopn2  23071  restntr  23076  cnpnei  23158  cncls2  23167  perfcls  23259  cmpsublem  23293  cmpsub  23294  cmpcld  23296  uncmp  23297  hauscmplem  23300  cmpfi  23302  nconnsubb  23317  clsconn  23324  hausllycmp  23388  1stckgenlem  23447  txbas  23461  ptbasfi  23475  txcnpi  23502  ptcnp  23516  txcmplem1  23535  txcmplem2  23536  xkococnlem  23553  qtopcld  23607  fbasssin  23730  fbssint  23732  fbun  23734  fbasrn  23778  filufint  23814  ufinffr  23823  ufildr  23825  ustval  24097  trust  24124  elmopn  24337  neibl  24396  cfilucfil  24454  icccmplem1  24718  icccmplem2  24719  bndth  24864  isphtpc  24900  metcld  25213  bcthlem1  25231  bcth  25236  ovolfioo  25375  ovolficc  25376  elovolmr  25384  ovoliunlem3  25412  ovolicc2  25430  volsuplem  25463  dyadmax  25506  dyadmbllem  25507  dyadmbl  25508  precsexlem6  28121  precsexlem7  28122  incistruhgr  29013  edgssv2  29132  wksfval  29544  2wlkdlem9  29871  3wlkdlem9  30104  sspval  30659  ubth  30809  orthin  31382  chssoc  31432  chsscon3  31436  chsscon1  31437  h1datom  31518  pjoml6i  31525  osum  31581  spansncv  31589  pjcjt2  31628  pjopyth  31656  hstel2  32155  hstle  32166  stj  32171  dmdbr5  32244  mdslmd1lem1  32261  atord  32324  chirredlem4  32329  atcvat4i  32333  mdsymlem2  32340  mdsymlem3  32341  mdsymlem8  32346  padct  32650  ssnnssfz  32717  pwrssmgc  32933  lindspropd  33361  idlsrgval  33481  constr01  33739  constrmon  33741  constrextdg2lem  33745  constrextdg2  33746  constrfiss  33748  tpr2rico  33909  ordtrestNEW  33918  sigaval  34108  issiga  34109  issgon  34120  oms0  34295  omssubadd  34298  subgrwlk  35126  umgr2cycllem  35134  kur14  35210  cvmliftlem15  35292  satfsschain  35358  mclsrcl  35555  mclsval  35557  ivthALT  36330  isfne  36334  topfne  36349  neibastop3  36357  tailfb  36372  filnetlem1  36373  filnetlem4  36376  relowlssretop  37358  rdgssun  37373  poimirlem24  37645  mblfinlem2  37659  sstotbnd2  37775  sstotbnd  37776  sstotbnd3  37777  ssbnd  37789  cntotbnd  37797  cnpwstotbnd  37798  ismtyres  37809  heibor1lem  37810  heiborlem1  37812  heiborlem6  37817  heiborlem8  37819  exidreslem  37878  scottexf  38169  scott0f  38170  cnvref4  38339  dfrefrels2  38511  dfrefrel2  38513  lshpcmp  38988  lsmsat  39008  lsmsatcv  39010  lfl1dim  39121  lfl1dim2N  39122  lkrss2N  39169  psubspset  39745  paddss  39846  psubclsetN  39937  dilfsetN  40153  dilsetN  40154  diaglbN  41056  dibglbN  41167  dihlspsnat  41334  dihglb2  41343  dochffval  41350  dochfval  41351  dochvalr  41358  dochord2N  41372  dochsncom  41383  dihjat1lem  41429  dvh4dimat  41439  dvh3dimatN  41440  dvh2dimatN  41441  dochexmidlem1  41461  lpolsetN  41483  lpolconN  41488  hdmaplkr  41914  hdmapoc  41932  hlhillcs  41959  ismrc  42696  incssnn0  42706  nacsfix  42707  hbt  43126  oacl2g  43326  omcl2  43329  ofoaf  43351  naddwordnexlem4  43397  ss2iundf  43655  clsk1indlem1  44041  clsk1independent  44042  isotone1  44044  isotone2  44045  ntrclsiso  44063  ntrclsk2  44064  scottelrankd  44243  ssinc  45088  uzfissfz  45329  stoweidlem50  46055  stoweidlem57  46062  fourierdlem20  46132  fourierdlem50  46161  fourierdlem64  46175  fourierdlem86  46197  fourierdlem103  46214  fourierdlem104  46215  ovnval  46546  hoicvrrex  46561  ovnlecvr  46563  ovncvrrp  46569  ovnsubaddlem1  46575  hoidmvlelem3  46602  hoidmvle  46605  ovnhoilem1  46606  ovnhoi  46608  ovnlecvr2  46615  ovncvr2  46616  hspmbl  46634  ovolval4lem2  46655  ovolval5lem2  46658  ovolval5lem3  46659  ovolval5  46660  ovnovollem1  46661  ovnovollem2  46662  sprsymrelfvlem  47495  grlimgrtri  47999  grilcbri2  48007  uspgrsprf  48138  uspgrsprfo  48140  ssnn0ssfz  48341  lincfsuppcl  48406  iunlub  48813  lubeldm2d  48950  glbeldm2d  48951