Theorem sseq12d 3950

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
sseq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
sseq12d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	sseq1d 3948	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3949	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 278	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  3sstr3d  3963  3sstr4d  3964  sscon34b  4225  ssdifeq0  4414  relcnvtrg  6159  knatar  7208  suppfnss  7976  funsssuppss  7977  csbfrecsg  8071  smogt  8169  oawordri  8343  omwordi  8364  omwordri  8365  oewordi  8384  oewordri  8385  oeworde  8386  nnawordi  8414  nnmwordi  8428  nnmwordri  8429  sbthlem2  8824  sbth  8833  sbthfi  8942  marypha2lem3  9126  hartogslem1  9231  inf3lem1  9316  tcrank  9573  alephle  9775  cfsmolem  9957  isfin3ds  10016  fin23lem17  10025  fin23lem39  10037  isf32lem1  10040  isf32lem2  10041  isf32lem11  10050  isf33lem  10053  isf34lem7  10066  isf34lem6  10067  fin1a2lem13  10099  itunitc1  10107  dominf  10132  dcomex  10134  axdc2lem  10135  dominfac  10260  fpwwe2cbv  10317  fpwwe2lem2  10319  fpwwecbv  10331  fpwwelem  10332  canthwelem  10337  canthwe  10338  wunex2  10425  swrdval  14284  trcleq2lem  14630  dfrtrcl2  14701  vdwpc  16609  vdwlem1  16610  vdwlem6  16615  vdwlem7  16616  vdwlem8  16617  isstruct2  16778  ressval  16870  mreexexlemd  17270  isacs1i  17283  isssc  17449  ssc2  17451  fullfunc  17538  fthfunc  17539  isps  18201  istsr  18216  isdir  18231  gsumvalx  18275  efgi2  19246  dmdprd  19516  dprdss  19547  dmdprdpr  19567  mhpfval  21239  scmatdmat  21572  basis1  22008  baspartn  22012  eltg  22015  cncls  22333  ispnrm  22398  1stcfb  22504  2ndcctbss  22514  1stcelcls  22520  subislly  22540  kgenidm  22606  ptpjpre1  22630  txcmplem2  22701  flimval  23022  flimcf  23041  fclscf  23084  metss  23570  isngp  23658  iscph  24239  cphsscph  24320  equivcau  24369  caubl  24377  caublcls  24378  ovoliunlem3  24573  volsuplem  24624  volsup  24625  dyaddisj  24665  itg1climres  24784  isausgr  27437  issubgr  27541  subgrprop3  27546  cusgrfilem1  27725  wkslem1  27877  wkslem2  27878  iswlk  27880  wlkres  27940  redwlk  27942  wlkp1lem8  27950  wlkdlem2  27953  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  crctcshwlkn0lem6  28081  2wlkdlem10  28201  3wlkdlem10  28434  eupthseg  28471  issh  29471  isch  29485  hsupss  29604  shslej  29643  shlub  29677  ledi  29803  pjoi0  29980  mdbr4  30561  dmdbr4  30569  dmdi4  30570  dmdbr5  30571  mdslle1i  30580  mdslle2i  30581  mdslmd1lem1  30588  mdslmd1lem2  30589  mdslmd1lem3  30590  mdslmd1lem4  30591  mdslmd1i  30592  sumdmdlem2  30682  resvval  31428  zhmnrg  31817  ispisys  32020  pfxwlk  32985  cvmliftlem3  33149  ismfs  33411  dfttrcl2  33710  naddssim  33764  naddss2  33769  rdgssun  35476  poimirlem32  35736  volsupnfl  35749  elrefrels2  36562  refreleq  36565  elcnvrefrels2  36575  dfsymrels2  36586  dfsymrel2  36590  elsymrels2  36594  symreleq  36599  elrefsymrels2  36610  dftrrels2  36616  dftrrel2  36618  eltrrels2  36620  trreleq  36623  eleqvrels2  36632  lssatle  36956  pmaple  37702  2polcon4bN  37859  ispautN  38040  diaord  38988  dibord  39100  dihord6apre  39197  dihord3  39198  dihord4  39199  dihcnvord  39215  dvh4dimlem  39384  islpolN  39424  mapdordlem2  39578  mapdcnvordN  39599  mapdindp  39612  hdmaplkr  39854  ismrcd1  40436  ismrcd2  40437  ismrc  40439  incssnn0  40449  diophrw  40497  hbtlem5  40869  hbt  40871  rclexi  41112  rtrclex  41114  trclubgNEW  41115  rtrclexi  41118  cnvrcl0  41122  cnvtrcl0  41123  dfrtrcl5  41126  trcleq2lemRP  41127  trficl  41166  dfrcl2  41171  relexpss1d  41202  trclrelexplem  41208  brtrclfv2  41224  dfrtrcl3  41230  heeq12  41273  ntrk2imkb  41536  clsk3nimkb  41539  clsk1independent  41545  isotone1  41547  isotone2  41548  ntrclsss  41562  ntrclsiso  41566  ntrclsk2  41567  ntrclsk3  41569  scottabf  41747  ismnu  41768  ismnushort  41808  nzss  41824  iunincfi  42533  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  meaiuninclem  43908  meaiunincf  43911  meaiuninc3v  43912  meaiuninc3  43913  meaiininclem  43914  meaiininc  43915  caragenss  43932  carageniuncllem1  43949  ovnsslelem  43988  hoidmvle  44028  ovnhoilem2  44030  hoiqssbl  44053  ovolval5lem2  44081  ovolval5lem3  44082  vonioolem2  44109  vonicclem2  44112  uspgrsprf  45196  scmsuppss  45596