Theorem sseq12d 4011

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  3sstr3d  4024  3sstr4d  4025  sscon34b  4290  ssdifeq0  4482  relcnvtrg  6264  knatar  7359  suppfnss  8187  funsssuppss  8188  csbfrecsg  8283  smogt  8381  oawordri  8564  omwordi  8585  omwordri  8586  oewordi  8605  oewordri  8606  oeworde  8607  nnawordi  8635  nnmwordi  8649  nnmwordri  8650  naddssim  8699  naddss2  8704  sbthlem2  9102  sbth  9111  sbthfi  9220  marypha2lem3  9454  hartogslem1  9559  inf3lem1  9645  dfttrcl2  9741  tcrank  9901  alephle  10105  cfsmolem  10287  isfin3ds  10346  fin23lem17  10355  fin23lem39  10367  isf32lem1  10370  isf32lem2  10371  isf32lem11  10380  isf33lem  10383  isf34lem7  10396  isf34lem6  10397  fin1a2lem13  10429  itunitc1  10437  dominf  10462  dcomex  10464  axdc2lem  10465  dominfac  10590  fpwwe2cbv  10647  fpwwe2lem2  10649  fpwwecbv  10661  fpwwelem  10662  canthwelem  10667  canthwe  10668  wunex2  10755  swrdval  14619  trcleq2lem  14964  dfrtrcl2  15035  vdwpc  16942  vdwlem1  16943  vdwlem6  16948  vdwlem7  16949  vdwlem8  16950  isstruct2  17111  ressval  17205  mreexexlemd  17617  isacs1i  17630  isssc  17796  ssc2  17798  fullfunc  17888  fthfunc  17889  isps  18553  istsr  18568  isdir  18583  gsumvalx  18629  efgi2  19673  dmdprd  19948  dprdss  19979  dmdprdpr  19999  mhpfval  22056  scmatdmat  22410  basis1  22846  baspartn  22850  eltg  22853  cncls  23171  ispnrm  23236  1stcfb  23342  2ndcctbss  23352  1stcelcls  23358  subislly  23378  kgenidm  23444  ptpjpre1  23468  txcmplem2  23539  flimval  23860  flimcf  23879  fclscf  23922  metss  24410  isngp  24498  iscph  25091  cphsscph  25172  equivcau  25221  caubl  25229  caublcls  25230  ovoliunlem3  25426  volsuplem  25477  volsup  25478  dyaddisj  25518  itg1climres  25637  negsbdaylem  27961  isausgr  28970  issubgr  29077  subgrprop3  29082  cusgrfilem1  29262  wkslem1  29414  wkslem2  29415  iswlk  29417  wlkres  29477  redwlk  29479  wlkp1lem8  29487  wlkdlem2  29490  crctcshwlkn0lem4  29617  crctcshwlkn0lem5  29618  crctcshwlkn0lem6  29619  2wlkdlem10  29739  3wlkdlem10  29972  eupthseg  30009  issh  31011  isch  31025  hsupss  31144  shslej  31183  shlub  31217  ledi  31343  pjoi0  31520  mdbr4  32101  dmdbr4  32109  dmdi4  32110  dmdbr5  32111  mdslle1i  32120  mdslle2i  32121  mdslmd1lem1  32128  mdslmd1lem2  32129  mdslmd1lem3  32130  mdslmd1lem4  32131  mdslmd1i  32132  sumdmdlem2  32222  resvval  33032  zhmnrg  33558  ispisys  33761  pfxwlk  34723  cvmliftlem3  34887  ismfs  35149  rdgssun  36847  poimirlem32  37114  volsupnfl  37127  elrefrels2  37979  refreleq  37982  elcnvrefrels2  37995  dfsymrels2  38006  dfsymrel2  38010  elsymrels2  38014  symreleq  38019  elrefsymrels2  38030  dftrrels2  38036  dftrrel2  38038  eltrrels2  38040  trreleq  38043  eleqvrels2  38053  lssatle  38476  pmaple  39223  2polcon4bN  39380  ispautN  39561  diaord  40509  dibord  40621  dihord6apre  40718  dihord3  40719  dihord4  40720  dihcnvord  40736  dvh4dimlem  40905  islpolN  40945  mapdordlem2  41099  mapdcnvordN  41120  mapdindp  41133  hdmaplkr  41375  ismrcd1  42090  ismrcd2  42091  ismrc  42093  incssnn0  42103  diophrw  42151  hbtlem5  42524  hbt  42526  naddgeoa  42796  minregex  42936  minregex2  42937  rclexi  43017  rtrclex  43019  trclubgNEW  43020  rtrclexi  43023  cnvrcl0  43027  cnvtrcl0  43028  dfrtrcl5  43031  trcleq2lemRP  43032  trficl  43071  dfrcl2  43076  relexpss1d  43107  trclrelexplem  43113  brtrclfv2  43129  dfrtrcl3  43135  heeq12  43178  ntrk2imkb  43439  clsk3nimkb  43442  clsk1independent  43448  isotone1  43450  isotone2  43451  ntrclsss  43465  ntrclsiso  43469  ntrclsk2  43470  ntrclsk3  43472  scottabf  43649  ismnu  43670  ismnushort  43710  nzss  43726  iunincfi  44432  fourierdlem89  45555  fourierdlem90  45556  fourierdlem91  45557  meaiuninclem  45840  meaiunincf  45843  meaiuninc3v  45844  meaiuninc3  45845  meaiininclem  45846  meaiininc  45847  caragenss  45864  carageniuncllem1  45881  hoidmvle  45960  ovnhoilem2  45962  hoiqssbl  45985  ovolval5lem2  46013  vonioolem2  46041  vonicclem2  46044  uspgrsprf  47180  scmsuppss  47408