Theorem sseq12d 3955

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  3sstr3d  3968  3sstr4d  3969  sscon34b  4229  ssdifeq0  4418  relcnvtrg  6174  knatar  7237  suppfnss  8014  funsssuppss  8015  csbfrecsg  8109  smogt  8207  oawordri  8390  omwordi  8411  omwordri  8412  oewordi  8431  oewordri  8432  oeworde  8433  nnawordi  8461  nnmwordi  8475  nnmwordri  8476  sbthlem2  8880  sbth  8889  sbthfi  8994  marypha2lem3  9205  hartogslem1  9310  inf3lem1  9395  dfttrcl2  9491  tcrank  9651  alephle  9853  cfsmolem  10035  isfin3ds  10094  fin23lem17  10103  fin23lem39  10115  isf32lem1  10118  isf32lem2  10119  isf32lem11  10128  isf33lem  10131  isf34lem7  10144  isf34lem6  10145  fin1a2lem13  10177  itunitc1  10185  dominf  10210  dcomex  10212  axdc2lem  10213  dominfac  10338  fpwwe2cbv  10395  fpwwe2lem2  10397  fpwwecbv  10409  fpwwelem  10410  canthwelem  10415  canthwe  10416  wunex2  10503  swrdval  14365  trcleq2lem  14711  dfrtrcl2  14782  vdwpc  16690  vdwlem1  16691  vdwlem6  16696  vdwlem7  16697  vdwlem8  16698  isstruct2  16859  ressval  16953  mreexexlemd  17362  isacs1i  17375  isssc  17541  ssc2  17543  fullfunc  17631  fthfunc  17632  isps  18295  istsr  18310  isdir  18325  gsumvalx  18369  efgi2  19340  dmdprd  19610  dprdss  19641  dmdprdpr  19661  mhpfval  21338  scmatdmat  21673  basis1  22109  baspartn  22113  eltg  22116  cncls  22434  ispnrm  22499  1stcfb  22605  2ndcctbss  22615  1stcelcls  22621  subislly  22641  kgenidm  22707  ptpjpre1  22731  txcmplem2  22802  flimval  23123  flimcf  23142  fclscf  23185  metss  23673  isngp  23761  iscph  24343  cphsscph  24424  equivcau  24473  caubl  24481  caublcls  24482  ovoliunlem3  24677  volsuplem  24728  volsup  24729  dyaddisj  24769  itg1climres  24888  isausgr  27543  issubgr  27647  subgrprop3  27652  cusgrfilem1  27831  wkslem1  27983  wkslem2  27984  iswlk  27986  wlkres  28047  redwlk  28049  wlkp1lem8  28057  wlkdlem2  28060  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  crctcshwlkn0lem6  28189  2wlkdlem10  28309  3wlkdlem10  28542  eupthseg  28579  issh  29579  isch  29593  hsupss  29712  shslej  29751  shlub  29785  ledi  29911  pjoi0  30088  mdbr4  30669  dmdbr4  30677  dmdi4  30678  dmdbr5  30679  mdslle1i  30688  mdslle2i  30689  mdslmd1lem1  30696  mdslmd1lem2  30697  mdslmd1lem3  30698  mdslmd1lem4  30699  mdslmd1i  30700  sumdmdlem2  30790  resvval  31535  zhmnrg  31926  ispisys  32129  pfxwlk  33094  cvmliftlem3  33258  ismfs  33520  naddssim  33846  naddss2  33851  rdgssun  35558  poimirlem32  35818  volsupnfl  35831  elrefrels2  36642  refreleq  36645  elcnvrefrels2  36655  dfsymrels2  36666  dfsymrel2  36670  elsymrels2  36674  symreleq  36679  elrefsymrels2  36690  dftrrels2  36696  dftrrel2  36698  eltrrels2  36700  trreleq  36703  eleqvrels2  36712  lssatle  37036  pmaple  37782  2polcon4bN  37939  ispautN  38120  diaord  39068  dibord  39180  dihord6apre  39277  dihord3  39278  dihord4  39279  dihcnvord  39295  dvh4dimlem  39464  islpolN  39504  mapdordlem2  39658  mapdcnvordN  39679  mapdindp  39692  hdmaplkr  39934  ismrcd1  40527  ismrcd2  40528  ismrc  40530  incssnn0  40540  diophrw  40588  hbtlem5  40960  hbt  40962  minregex  41148  minregex2  41149  rclexi  41230  rtrclex  41232  trclubgNEW  41233  rtrclexi  41236  cnvrcl0  41240  cnvtrcl0  41241  dfrtrcl5  41244  trcleq2lemRP  41245  trficl  41284  dfrcl2  41289  relexpss1d  41320  trclrelexplem  41326  brtrclfv2  41342  dfrtrcl3  41348  heeq12  41391  ntrk2imkb  41654  clsk3nimkb  41657  clsk1independent  41663  isotone1  41665  isotone2  41666  ntrclsss  41680  ntrclsiso  41684  ntrclsk2  41685  ntrclsk3  41687  scottabf  41865  ismnu  41886  ismnushort  41926  nzss  41942  iunincfi  42651  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  meaiuninclem  44025  meaiunincf  44028  meaiuninc3v  44029  meaiuninc3  44030  meaiininclem  44031  meaiininc  44032  caragenss  44049  carageniuncllem1  44066  ovnsslelem  44105  hoidmvle  44145  ovnhoilem2  44147  hoiqssbl  44170  ovolval5lem2  44198  ovolval5lem3  44199  vonioolem2  44226  vonicclem2  44229  uspgrsprf  45319  scmsuppss  45719