Theorem sseq2d 3947

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  sseq12d  3948  sseqtrd  3955  sbcrel  5619  funimass2  6407  fnco  6437  fnssresb  6441  fnimaeq0  6453  foimacnv  6607  fvelimab  6712  ssimaexg  6724  knatar  7089  wfrdmcl  7946  wfrlem12  7949  onfununi  7961  oaordi  8155  oawordeulem  8163  oaass  8170  odi  8188  omass  8189  oen0  8195  oelim2  8204  nnaordi  8227  nnawordex  8246  pssnn  8720  fissuni  8813  dffi3  8879  cantnfle  9118  cantnflem1  9136  trcl  9154  r1sdom  9187  iscard2  9389  alephordi  9485  alephgeom  9493  cardaleph  9500  cardalephex  9501  ackbij2lem4  9653  cflm  9661  cfslbn  9678  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  coftr  9684  alephsing  9687  fin23lem28  9751  fin23lem30  9753  fin23lem33  9756  fin1a2lem9  9819  axdc3lem2  9862  ttukeylem5  9924  fpwwe2lem5  10045  pwfseqlem4a  10072  pwfseqlem4  10073  wunex2  10149  inar1  10186  sstskm  10253  fsuppmapnn0fiubex  13355  swrdnd  14007  swrd0  14011  repswswrd  14137  rtrclreclem1  14408  rtrclreclem2  14410  summolem2  15065  summo  15066  zsum  15067  sumz  15071  sumss  15073  fsumcvg3  15078  prodmolem2  15281  prodmo  15282  zprod  15283  prod1  15290  vdwlem1  16307  vdwlem12  16318  vdwlem13  16319  ramub2  16340  rami  16341  ramz2  16350  setsstruct2  16513  prdsval  16720  pwsle  16757  mrcuni  16884  gsumpropd  17880  gsumpropd2lem  17881  gsumress  17884  eqgfval  18320  sscntz  18448  resscntz  18454  lsmlub  18782  efgrelexlemb  18868  efgcpbllemb  18873  gsumval3a  19016  gsumzaddlem  19034  gsumzoppg  19057  dmdprd  19113  dprdcntz  19123  subgdmdprd  19149  subrgpropd  19563  islss  19699  lsslss  19726  lsspropd  19782  lsmelpr  19856  lbspropd  19864  lsslinds  20520  ltbval  20711  opsrval  20714  mhpval  20792  isbasisg  21552  tgval  21560  tgss3  21591  restbas  21763  tgrest  21764  restcld  21777  restopn2  21782  restntr  21787  cnpnei  21869  cncls2  21878  perfcls  21970  cmpsublem  22004  cmpsub  22005  cmpcld  22007  uncmp  22008  hauscmplem  22011  cmpfi  22013  nconnsubb  22028  clsconn  22035  hausllycmp  22099  1stckgenlem  22158  txbas  22172  ptbasfi  22186  txcnpi  22213  ptcnp  22227  txcmplem1  22246  txcmplem2  22247  xkococnlem  22264  qtopcld  22318  fbasssin  22441  fbssint  22443  fbun  22445  fbasrn  22489  filufint  22525  ufinffr  22534  ufildr  22536  ustval  22808  trust  22835  elmopn  23049  neibl  23108  cfilucfil  23166  icccmplem1  23427  icccmplem2  23428  bndth  23563  isphtpc  23599  metcld  23910  bcthlem1  23928  bcth  23933  ovolfioo  24071  ovolficc  24072  elovolmr  24080  ovoliunlem3  24108  ovolicc2  24126  volsuplem  24159  dyadmax  24202  dyadmbllem  24203  dyadmbl  24204  incistruhgr  26872  edgssv2  26988  wksfval  27399  2wlkdlem9  27720  3wlkdlem9  27953  sspval  28506  ubth  28656  orthin  29229  chssoc  29279  chsscon3  29283  chsscon1  29284  h1datom  29365  pjoml6i  29372  osum  29428  spansncv  29436  pjcjt2  29475  pjopyth  29503  hstel2  30002  hstle  30013  stj  30018  dmdbr5  30091  mdslmd1lem1  30108  atord  30171  chirredlem4  30176  atcvat4i  30180  mdsymlem2  30187  mdsymlem3  30188  mdsymlem8  30193  padct  30481  ssnnssfz  30536  pwrssmgc  30706  lindspropd  30997  idlsrgval  31056  tpr2rico  31265  ordtrestNEW  31274  sigaval  31480  issiga  31481  issgon  31492  oms0  31665  omssubadd  31668  subgrwlk  32492  umgr2cycllem  32500  kur14  32576  cvmliftlem15  32658  satfsschain  32724  mclsrcl  32921  mclsval  32923  trpredtr  33182  dftrpred3g  33185  frecseq123  33232  frrlem4  33239  ivthALT  33796  isfne  33800  topfne  33815  neibastop3  33823  tailfb  33838  filnetlem1  33839  filnetlem4  33842  csbwrecsg  34744  relowlssretop  34780  rdgssun  34795  poimirlem24  35081  mblfinlem2  35095  sstotbnd2  35212  sstotbnd  35213  sstotbnd3  35214  ssbnd  35226  cntotbnd  35234  cnpwstotbnd  35235  ismtyres  35246  heibor1lem  35247  heiborlem1  35249  heiborlem6  35254  heiborlem8  35256  exidreslem  35315  scottexf  35606  scott0f  35607  dfrefrels2  35913  dfrefrel2  35915  lshpcmp  36284  lsmsat  36304  lsmsatcv  36306  lfl1dim  36417  lfl1dim2N  36418  lkrss2N  36465  psubspset  37040  paddss  37141  psubclsetN  37232  dilfsetN  37448  dilsetN  37449  diaglbN  38351  dibglbN  38462  dihlspsnat  38629  dihglb2  38638  dochffval  38645  dochfval  38646  dochvalr  38653  dochord2N  38667  dochsncom  38678  dihjat1lem  38724  dvh4dimat  38734  dvh3dimatN  38735  dvh2dimatN  38736  dochexmidlem1  38756  lpolsetN  38778  lpolconN  38783  hdmaplkr  39209  hdmapoc  39227  hlhillcs  39254  ismrc  39642  incssnn0  39652  nacsfix  39653  hbt  40074  ss2iundf  40360  clsk1indlem1  40748  clsk1independent  40749  isotone1  40751  isotone2  40752  ntrclsiso  40770  ntrclsk2  40771  scottelrankd  40955  ssinc  41723  uzfissfz  41958  stoweidlem50  42692  stoweidlem57  42699  fourierdlem20  42769  fourierdlem50  42798  fourierdlem64  42812  fourierdlem86  42834  fourierdlem103  42851  fourierdlem104  42852  ovnval  43180  hoicvrrex  43195  ovnlecvr  43197  ovncvrrp  43203  ovnsubaddlem1  43209  hoidmvlelem3  43236  hoidmvle  43239  ovnhoilem1  43240  ovnhoi  43242  ovnlecvr2  43249  ovncvr2  43250  hspmbl  43268  ovolval4lem2  43289  ovolval5lem2  43292  ovolval5lem3  43293  ovolval5  43294  ovnovollem1  43295  ovnovollem2  43296  sprsymrelfvlem  44007  uspgrsprf  44374  uspgrsprfo  44376  ssnn0ssfz  44751  lincfsuppcl  44822