Theorem sseq12d 3967

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  sscon34b  4253  ssdifeq0  4445  relcnvtrgOLD  6268  knatar  7364  suppfnss  8191  funsssuppss  8192  csbfrecsg  8287  smogt  8360  oawordri  8541  omwordi  8562  omwordri  8563  oewordi  8583  oewordri  8584  oeworde  8585  nnawordi  8613  nnmwordi  8627  nnmwordri  8628  naddssim  8678  naddss2  8683  sbthlem2  9090  sbth  9099  sbthfi  9197  marypha2lem3  9411  hartogslem1  9518  inf3lem1  9611  dfttrcl2  9707  tcrank  9870  scottabf  9882  alephle  10095  cfsmolem  10276  isfin3ds  10335  fin23lem17  10344  fin23lem39  10356  isf32lem1  10359  isf32lem2  10360  isf32lem11  10369  isf33lem  10372  isf34lem7  10385  isf34lem6  10386  fin1a2lem13  10418  itunitc1  10426  dominf  10451  dcomex  10453  axdc2lem  10454  dominfac  10586  fpwwe2cbv  10643  fpwwe2lem2  10645  fpwwe2lem4  10647  fpwwecbv  10657  fpwwelem  10658  canthwelem  10663  canthwe  10664  pwfseqlem4  10675  wunex2  10751  swrdval  14715  trcleq2lem  15068  dfrtrcl2  15139  vdwpc  17078  vdwlem1  17079  vdwlem6  17084  vdwlem7  17085  vdwlem8  17086  isstruct2  17247  ressval  17331  mreexexlemd  17738  isacs1i  17751  isssc  17915  ssc2  17917  fullfunc  18003  fthfunc  18004  isps  18662  istsr  18677  isdir  18692  gsumvalx  18784  efgi2  19858  dmdprd  20133  dprdss  20164  dmdprdpr  20184  mhpfval  22372  scmatdmat  22743  basis1  23181  baspartn  23185  eltg  23188  cncls  23505  ispnrm  23570  1stcfb  23676  2ndcctbss  23687  1stcelcls  23693  subislly  23713  kgenidm  23779  ptpjpre1  23803  txcmplem2  23874  flimval  24195  flimcf  24214  fclscf  24257  metss  24740  isngp  24828  iscph  25404  cphsscph  25485  equivcau  25534  caubl  25542  caublcls  25543  ovoliunlem3  25738  volsuplem  25789  volsup  25790  dyaddisj  25830  itg1climres  25948  addbdaylem  28290  addbday  28291  negbdaylem  28329  addonbday  28552  bdaypw2n0bndlem  28736  bdaypw2n0bnd  28737  isausgr  29632  issubgr  29739  subgrprop3  29744  cusgrfilem1  29923  wkslem1  30075  wkslem2  30076  iswlk  30078  wlkres  30136  redwlk  30138  wlkp1lem8  30146  wlkdlem2  30149  pfxwlk  30153  crctcshwlkn0lem4  30289  crctcshwlkn0lem5  30290  crctcshwlkn0lem6  30291  2wlkdlem10  30411  3wlkdlem10  30657  eupthseg  30694  issh  31697  isch  31711  hsupss  31830  shslej  31869  shlub  31903  ledi  32029  pjoi0  32206  mdbr4  32787  dmdbr4  32795  dmdi4  32796  dmdbr5  32797  mdslle1i  32806  mdslle2i  32807  mdslmd1lem1  32814  mdslmd1lem2  32815  mdslmd1lem3  32816  mdslmd1lem4  32817  mdslmd1i  32818  sumdmdlem2  32908  resvval  33777  zhmnrg  34483  ispisys  34671  cvmliftlem3  35874  ismfs  36136  nmuladdss  36801  rdgssun  38140  poimirlem32  38409  volsupnfl  38422  elrefrels2  39354  refreleq  39357  elcnvrefrels2  39370  dfsymrels2  39381  dfsymrel2  39389  elsymrels2  39393  symreleq  39398  elrefsymrels2  39409  dftrrels2  39415  dftrrel2  39417  eltrrels2  39419  trreleq  39422  eleqvrels2  39432  lssatle  39896  pmaple  40642  2polcon4bN  40799  ispautN  40980  diaord  41928  dibord  42040  dihord6apre  42137  dihord3  42138  dihord4  42139  dihcnvord  42155  dvh4dimlem  42324  islpolN  42364  mapdordlem2  42518  mapdcnvordN  42539  mapdindp  42552  hdmaplkr  42794  ismrcd1  43551  ismrcd2  43552  ismrc  43554  incssnn0  43564  diophrw  43612  hbtlem5  43977  hbt  43979  naddgeoa  44243  minregex  44382  minregex2  44383  rclexi  44463  rtrclex  44465  trclubgNEW  44466  rtrclexi  44469  cnvrcl0  44473  cnvtrcl0  44474  dfrtrcl5  44477  trcleq2lemRP  44478  trficl  44517  dfrcl2  44522  relexpss1d  44553  trclrelexplem  44559  brtrclfv2  44575  dfrtrcl3  44581  heeq12  44624  ntrk2imkb  44885  clsk3nimkb  44888  clsk1independent  44894  isotone1  44896  isotone2  44897  ntrclsss  44911  ntrclsiso  44915  ntrclsk2  44916  ntrclsk3  44918  ismnu  45093  ismnushort  45133  nzss  45149  iunincfi  45934  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  meaiuninclem  47316  meaiunincf  47319  meaiuninc3v  47320  meaiuninc3  47321  meaiininclem  47322  meaiininc  47323  caragenss  47340  carageniuncllem1  47357  hoidmvle  47436  ovnhoilem2  47438  hoiqssbl  47461  ovolval5lem2  47489  vonioolem2  47517  vonicclem2  47520  isisubgr  48786  uspgrsprf  49070  scmsuppss  49309  setc1onsubc  50536