Theorem sseq12d 4028

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  3sstr3d  4041  3sstr4d  4042  sscon34b  4309  ssdifeq0  4492  relcnvtrg  6287  knatar  7376  suppfnss  8212  funsssuppss  8213  csbfrecsg  8307  smogt  8405  oawordri  8586  omwordi  8607  omwordri  8608  oewordi  8627  oewordri  8628  oeworde  8629  nnawordi  8657  nnmwordi  8671  nnmwordri  8672  naddssim  8721  naddss2  8726  sbthlem2  9122  sbth  9131  sbthfi  9236  marypha2lem3  9474  hartogslem1  9579  inf3lem1  9665  dfttrcl2  9761  tcrank  9921  alephle  10125  cfsmolem  10307  isfin3ds  10366  fin23lem17  10375  fin23lem39  10387  isf32lem1  10390  isf32lem2  10391  isf32lem11  10400  isf33lem  10403  isf34lem7  10416  isf34lem6  10417  fin1a2lem13  10449  itunitc1  10457  dominf  10482  dcomex  10484  axdc2lem  10485  dominfac  10610  fpwwe2cbv  10667  fpwwe2lem2  10669  fpwwe2lem4  10671  fpwwecbv  10681  fpwwelem  10682  canthwelem  10687  canthwe  10688  pwfseqlem4  10699  wunex2  10775  swrdval  14677  trcleq2lem  15026  dfrtrcl2  15097  vdwpc  17013  vdwlem1  17014  vdwlem6  17019  vdwlem7  17020  vdwlem8  17021  isstruct2  17182  ressval  17276  mreexexlemd  17688  isacs1i  17701  isssc  17867  ssc2  17869  fullfunc  17959  fthfunc  17960  isps  18625  istsr  18640  isdir  18655  gsumvalx  18701  efgi2  19757  dmdprd  20032  dprdss  20063  dmdprdpr  20083  mhpfval  22159  scmatdmat  22536  basis1  22972  baspartn  22976  eltg  22979  cncls  23297  ispnrm  23362  1stcfb  23468  2ndcctbss  23478  1stcelcls  23484  subislly  23504  kgenidm  23570  ptpjpre1  23594  txcmplem2  23665  flimval  23986  flimcf  24005  fclscf  24048  metss  24536  isngp  24624  iscph  25217  cphsscph  25298  equivcau  25347  caubl  25355  caublcls  25356  ovoliunlem3  25552  volsuplem  25603  volsup  25604  dyaddisj  25644  itg1climres  25763  addsbdaylem  28063  addsbday  28064  negsbdaylem  28102  isausgr  29195  issubgr  29302  subgrprop3  29307  cusgrfilem1  29487  wkslem1  29639  wkslem2  29640  iswlk  29642  wlkres  29702  redwlk  29704  wlkp1lem8  29712  wlkdlem2  29715  crctcshwlkn0lem4  29842  crctcshwlkn0lem5  29843  crctcshwlkn0lem6  29844  2wlkdlem10  29964  3wlkdlem10  30197  eupthseg  30234  issh  31236  isch  31250  hsupss  31369  shslej  31408  shlub  31442  ledi  31568  pjoi0  31745  mdbr4  32326  dmdbr4  32334  dmdi4  32335  dmdbr5  32336  mdslle1i  32345  mdslle2i  32346  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd1lem3  32355  mdslmd1lem4  32356  mdslmd1i  32357  sumdmdlem2  32447  resvval  33332  zhmnrg  33927  ispisys  34132  pfxwlk  35107  cvmliftlem3  35271  ismfs  35533  rdgssun  37360  poimirlem32  37638  volsupnfl  37651  elrefrels2  38499  refreleq  38502  elcnvrefrels2  38515  dfsymrels2  38526  dfsymrel2  38530  elsymrels2  38534  symreleq  38539  elrefsymrels2  38550  dftrrels2  38556  dftrrel2  38558  eltrrels2  38560  trreleq  38563  eleqvrels2  38573  lssatle  38996  pmaple  39743  2polcon4bN  39900  ispautN  40081  diaord  41029  dibord  41141  dihord6apre  41238  dihord3  41239  dihord4  41240  dihcnvord  41256  dvh4dimlem  41425  islpolN  41465  mapdordlem2  41619  mapdcnvordN  41640  mapdindp  41653  hdmaplkr  41895  ismrcd1  42685  ismrcd2  42686  ismrc  42688  incssnn0  42698  diophrw  42746  hbtlem5  43116  hbt  43118  naddgeoa  43383  minregex  43523  minregex2  43524  rclexi  43604  rtrclex  43606  trclubgNEW  43607  rtrclexi  43610  cnvrcl0  43614  cnvtrcl0  43615  dfrtrcl5  43618  trcleq2lemRP  43619  trficl  43658  dfrcl2  43663  relexpss1d  43694  trclrelexplem  43700  brtrclfv2  43716  dfrtrcl3  43722  heeq12  43765  ntrk2imkb  44026  clsk3nimkb  44029  clsk1independent  44035  isotone1  44037  isotone2  44038  ntrclsss  44052  ntrclsiso  44056  ntrclsk2  44057  ntrclsk3  44059  scottabf  44235  ismnu  44256  ismnushort  44296  nzss  44312  iunincfi  45033  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  meaiuninclem  46435  meaiunincf  46438  meaiuninc3v  46439  meaiuninc3  46440  meaiininclem  46441  meaiininc  46442  caragenss  46459  carageniuncllem1  46476  hoidmvle  46555  ovnhoilem2  46557  hoiqssbl  46580  ovolval5lem2  46608  vonioolem2  46636  vonicclem2  46639  isisubgr  47785  uspgrsprf  47989  scmsuppss  48215