Theorem sseq12d 3980

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  sscon34b  4267  ssdifeq0  4450  relcnvtrg  6239  knatar  7332  suppfnss  8168  funsssuppss  8169  csbfrecsg  8263  smogt  8336  oawordri  8514  omwordi  8535  omwordri  8536  oewordi  8555  oewordri  8556  oeworde  8557  nnawordi  8585  nnmwordi  8599  nnmwordri  8600  naddssim  8649  naddss2  8654  sbthlem2  9052  sbth  9061  sbthfi  9163  marypha2lem3  9388  hartogslem1  9495  inf3lem1  9581  dfttrcl2  9677  tcrank  9837  alephle  10041  cfsmolem  10223  isfin3ds  10282  fin23lem17  10291  fin23lem39  10303  isf32lem1  10306  isf32lem2  10307  isf32lem11  10316  isf33lem  10319  isf34lem7  10332  isf34lem6  10333  fin1a2lem13  10365  itunitc1  10373  dominf  10398  dcomex  10400  axdc2lem  10401  dominfac  10526  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2lem4  10587  fpwwecbv  10597  fpwwelem  10598  canthwelem  10603  canthwe  10604  pwfseqlem4  10615  wunex2  10691  swrdval  14608  trcleq2lem  14957  dfrtrcl2  15028  vdwpc  16951  vdwlem1  16952  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  isstruct2  17119  ressval  17203  mreexexlemd  17605  isacs1i  17618  isssc  17782  ssc2  17784  fullfunc  17870  fthfunc  17871  isps  18527  istsr  18542  isdir  18557  gsumvalx  18603  efgi2  19655  dmdprd  19930  dprdss  19961  dmdprdpr  19981  mhpfval  22025  scmatdmat  22402  basis1  22837  baspartn  22841  eltg  22844  cncls  23161  ispnrm  23226  1stcfb  23332  2ndcctbss  23342  1stcelcls  23348  subislly  23368  kgenidm  23434  ptpjpre1  23458  txcmplem2  23529  flimval  23850  flimcf  23869  fclscf  23912  metss  24396  isngp  24484  iscph  25070  cphsscph  25151  equivcau  25200  caubl  25208  caublcls  25209  ovoliunlem3  25405  volsuplem  25456  volsup  25457  dyaddisj  25497  itg1climres  25615  addsbdaylem  27923  addsbday  27924  negsbdaylem  27962  isausgr  29091  issubgr  29198  subgrprop3  29203  cusgrfilem1  29383  wkslem1  29535  wkslem2  29536  iswlk  29538  wlkres  29598  redwlk  29600  wlkp1lem8  29608  wlkdlem2  29611  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  crctcshwlkn0lem6  29745  2wlkdlem10  29865  3wlkdlem10  30098  eupthseg  30135  issh  31137  isch  31151  hsupss  31270  shslej  31309  shlub  31343  ledi  31469  pjoi0  31646  mdbr4  32227  dmdbr4  32235  dmdi4  32236  dmdbr5  32237  mdslle1i  32246  mdslle2i  32247  mdslmd1lem1  32254  mdslmd1lem2  32255  mdslmd1lem3  32256  mdslmd1lem4  32257  mdslmd1i  32258  sumdmdlem2  32348  resvval  33301  zhmnrg  33955  ispisys  34142  pfxwlk  35111  cvmliftlem3  35274  ismfs  35536  rdgssun  37366  poimirlem32  37646  volsupnfl  37659  elrefrels2  38509  refreleq  38512  elcnvrefrels2  38525  dfsymrels2  38536  dfsymrel2  38540  elsymrels2  38544  symreleq  38549  elrefsymrels2  38560  dftrrels2  38566  dftrrel2  38568  eltrrels2  38570  trreleq  38573  eleqvrels2  38583  lssatle  39008  pmaple  39755  2polcon4bN  39912  ispautN  40093  diaord  41041  dibord  41153  dihord6apre  41250  dihord3  41251  dihord4  41252  dihcnvord  41268  dvh4dimlem  41437  islpolN  41477  mapdordlem2  41631  mapdcnvordN  41652  mapdindp  41665  hdmaplkr  41907  ismrcd1  42686  ismrcd2  42687  ismrc  42689  incssnn0  42699  diophrw  42747  hbtlem5  43117  hbt  43119  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  44229  ismnu  44250  ismnushort  44290  nzss  44306  iunincfi  45088  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  meaiuninclem  46478  meaiunincf  46481  meaiuninc3v  46482  meaiuninc3  46483  meaiininclem  46484  meaiininc  46485  caragenss  46502  carageniuncllem1  46519  hoidmvle  46598  ovnhoilem2  46600  hoiqssbl  46623  ovolval5lem2  46651  vonioolem2  46679  vonicclem2  46682  isisubgr  47862  uspgrsprf  48134  scmsuppss  48359  setc1onsubc  49591