Theorem sseq12d 3969

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 3967	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3968	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  sscon34b  4258  ssdifeq0  4441  relcnvtrg  6233  knatar  7313  suppfnss  8141  funsssuppss  8142  csbfrecsg  8236  smogt  8309  oawordri  8487  omwordi  8508  omwordri  8509  oewordi  8529  oewordri  8530  oeworde  8531  nnawordi  8559  nnmwordi  8573  nnmwordri  8574  naddssim  8623  naddss2  8628  sbthlem2  9028  sbth  9037  sbthfi  9135  marypha2lem3  9352  hartogslem1  9459  inf3lem1  9549  dfttrcl2  9645  tcrank  9808  alephle  10010  cfsmolem  10192  isfin3ds  10251  fin23lem17  10260  fin23lem39  10272  isf32lem1  10275  isf32lem2  10276  isf32lem11  10285  isf33lem  10288  isf34lem7  10301  isf34lem6  10302  fin1a2lem13  10334  itunitc1  10342  dominf  10367  dcomex  10369  axdc2lem  10370  dominfac  10496  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwecbv  10567  fpwwelem  10568  canthwelem  10573  canthwe  10574  pwfseqlem4  10585  wunex2  10661  swrdval  14579  trcleq2lem  14926  dfrtrcl2  14997  vdwpc  16920  vdwlem1  16921  vdwlem6  16926  vdwlem7  16927  vdwlem8  16928  isstruct2  17088  ressval  17172  mreexexlemd  17579  isacs1i  17592  isssc  17756  ssc2  17758  fullfunc  17844  fthfunc  17845  isps  18503  istsr  18518  isdir  18533  gsumvalx  18613  efgi2  19666  dmdprd  19941  dprdss  19972  dmdprdpr  19992  mhpfval  22093  scmatdmat  22471  basis1  22906  baspartn  22910  eltg  22913  cncls  23230  ispnrm  23295  1stcfb  23401  2ndcctbss  23411  1stcelcls  23417  subislly  23437  kgenidm  23503  ptpjpre1  23527  txcmplem2  23598  flimval  23919  flimcf  23938  fclscf  23981  metss  24464  isngp  24552  iscph  25138  cphsscph  25219  equivcau  25268  caubl  25276  caublcls  25277  ovoliunlem3  25473  volsuplem  25524  volsup  25525  dyaddisj  25565  itg1climres  25683  addbdaylem  28025  addbday  28026  negbdaylem  28064  addonbday  28287  bdaypw2n0bndlem  28471  bdaypw2n0bnd  28472  isausgr  29249  issubgr  29356  subgrprop3  29361  cusgrfilem1  29541  wkslem1  29693  wkslem2  29694  iswlk  29696  wlkres  29754  redwlk  29756  wlkp1lem8  29764  wlkdlem2  29767  crctcshwlkn0lem4  29898  crctcshwlkn0lem5  29899  crctcshwlkn0lem6  29900  2wlkdlem10  30020  3wlkdlem10  30256  eupthseg  30293  issh  31295  isch  31309  hsupss  31428  shslej  31467  shlub  31501  ledi  31627  pjoi0  31804  mdbr4  32385  dmdbr4  32393  dmdi4  32394  dmdbr5  32395  mdslle1i  32404  mdslle2i  32405  mdslmd1lem1  32412  mdslmd1lem2  32413  mdslmd1lem3  32414  mdslmd1lem4  32415  mdslmd1i  32416  sumdmdlem2  32506  resvval  33421  zhmnrg  34142  ispisys  34329  pfxwlk  35337  cvmliftlem3  35500  ismfs  35762  rdgssun  37622  poimirlem32  37892  volsupnfl  37905  elrefrels2  38838  refreleq  38841  elcnvrefrels2  38854  dfsymrels2  38865  dfsymrel2  38873  elsymrels2  38877  symreleq  38882  elrefsymrels2  38893  dftrrels2  38899  dftrrel2  38901  eltrrels2  38903  trreleq  38906  eleqvrels2  38916  lssatle  39380  pmaple  40126  2polcon4bN  40283  ispautN  40464  diaord  41412  dibord  41524  dihord6apre  41621  dihord3  41622  dihord4  41623  dihcnvord  41639  dvh4dimlem  41808  islpolN  41848  mapdordlem2  42002  mapdcnvordN  42023  mapdindp  42036  hdmaplkr  42278  ismrcd1  43044  ismrcd2  43045  ismrc  43047  incssnn0  43057  diophrw  43105  hbtlem5  43474  hbt  43476  naddgeoa  43740  minregex  43879  minregex2  43880  rclexi  43960  rtrclex  43962  trclubgNEW  43963  rtrclexi  43966  cnvrcl0  43970  cnvtrcl0  43971  dfrtrcl5  43974  trcleq2lemRP  43975  trficl  44014  dfrcl2  44019  relexpss1d  44050  trclrelexplem  44056  brtrclfv2  44072  dfrtrcl3  44078  heeq12  44121  ntrk2imkb  44382  clsk3nimkb  44385  clsk1independent  44391  isotone1  44393  isotone2  44394  ntrclsss  44408  ntrclsiso  44412  ntrclsk2  44413  ntrclsk3  44415  scottabf  44585  ismnu  44606  ismnushort  44646  nzss  44662  iunincfi  45442  fourierdlem89  46542  fourierdlem90  46543  fourierdlem91  46544  meaiuninclem  46827  meaiunincf  46830  meaiuninc3v  46831  meaiuninc3  46832  meaiininclem  46833  meaiininc  46834  caragenss  46851  carageniuncllem1  46868  hoidmvle  46947  ovnhoilem2  46949  hoiqssbl  46972  ovolval5lem2  47000  vonioolem2  47028  vonicclem2  47031  isisubgr  48211  uspgrsprf  48495  scmsuppss  48720  setc1onsubc  49950