Theorem sseq12d 3597

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  3sstr3d  3610  3sstr4d  3611  ssdifeq0  4003  relcnvtr  5572  knatar  6507  suppfnss  7207  funsssuppss  7208  smogt  7351  oawordri  7517  omwordi  7538  omwordri  7539  oewordi  7558  oewordri  7559  oeworde  7560  nnawordi  7588  nnmwordi  7602  nnmwordri  7603  sbthlem2  7956  sbth  7965  marypha2lem3  8226  hartogslem1  8330  inf3lem1  8408  tcrank  8630  alephle  8794  cfsmolem  8975  isfin3ds  9034  fin23lem17  9043  fin23lem39  9055  isf32lem1  9058  isf32lem2  9059  isf32lem11  9068  isf33lem  9071  isf34lem7  9084  isf34lem6  9085  fin1a2lem13  9117  itunitc1  9125  dominf  9150  dcomex  9152  axdc2lem  9153  dominfac  9274  fpwwe2cbv  9331  fpwwe2lem2  9333  fpwwecbv  9345  fpwwelem  9346  canthwelem  9351  canthwe  9352  wunex2  9439  swrdval  13269  trcleq2lem  13578  dfrtrcl2  13650  vdwpc  15522  vdwlem1  15523  vdwlem6  15528  vdwlem7  15529  vdwlem8  15530  isstruct2  15704  ressval  15754  mreexexlemd  16127  isacs1i  16141  isssc  16303  ssc2  16305  fullfunc  16389  fthfunc  16390  isps  17025  istsr  17040  isdir  17055  gsumvalx  17093  efgi2  17961  dmdprd  18220  dprdss  18251  dmdprdpr  18271  scmatdmat  20140  basis1  20565  baspartn  20569  eltg  20572  cncls  20888  ispnrm  20953  1stcfb  21058  2ndcctbss  21068  1stcelcls  21074  subislly  21094  kgenidm  21160  ptpjpre1  21184  txcmplem2  21255  flimval  21577  flimcf  21596  fclscf  21639  metss  22123  isngp  22210  iscph  22778  equivcau  22906  caubl  22914  caublcls  22915  ovoliunlem3  23079  volsuplem  23130  volsup  23131  dyaddisj  23170  itg1climres  23287  edgss  25881  isausgra  25883  cusgrafilem1  26007  issh  27449  isch  27463  hsupss  27584  shslej  27623  shlub  27657  ledi  27783  pjoi0  27960  mdbr4  28541  dmdbr4  28549  dmdi4  28550  dmdbr5  28551  mdslle1i  28560  mdslle2i  28561  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd1lem3  28570  mdslmd1lem4  28571  mdslmd1i  28572  sumdmdlem2  28662  resvval  29158  zhmnrg  29339  ispisys  29542  cvmliftlem3  30523  ismfs  30700  poimirlem32  32611  volsupnfl  32624  lssatle  33320  pmaple  34065  2polcon4bN  34222  ispautN  34403  diaord  35354  dibord  35466  dihord6apre  35563  dihord3  35564  dihord4  35565  dihcnvord  35581  dvh4dimlem  35750  islpolN  35790  mapdordlem2  35944  mapdcnvordN  35965  mapdindp  35978  hdmaplkr  36223  ismrcd1  36279  ismrcd2  36280  ismrc  36282  incssnn0  36292  diophrw  36340  hbtlem5  36717  hbt  36719  rclexi  36941  rtrclex  36943  trclubgNEW  36944  rtrclexi  36947  cnvrcl0  36951  cnvtrcl0  36952  dfrtrcl5  36955  trcleq2lemRP  36956  trficl  36980  dfrcl2  36985  relexpss1d  37016  trclrelexplem  37022  brtrclfv2  37038  dfrtrcl3  37044  heeq12  37090  sscon34b  37337  ntrk2imkb  37355  clsk3nimkb  37358  clsk1independent  37364  isotone1  37366  isotone2  37367  ntrclsss  37381  ntrclsiso  37385  ntrclsk2  37386  ntrclsk3  37388  nzss  37538  iunincfi  38300  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  meaiuninclem  39373  meaiininclem  39376  meaiininc  39377  caragenss  39394  carageniuncllem1  39411  ovnsslelem  39450  hoidmvle  39490  ovnhoilem2  39492  hoiqssbl  39515  ovolval5lem2  39543  ovolval5lem3  39544  vonioolem2  39572  vonicclem2  39575  isausgr  40394  issubgr  40495  subgrprop3  40500  cusgrfilem1  40671  1wlkslem1  40809  1wlkslem2  40810  is1wlk  40813  1wlkres  40879  red1wlk  40881  1wlkp1lem8  40889  1wlkdlem2  40892  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem5  41017  crctcsh1wlkn0lem6  41018  21wlkdlem10  41142  31wlkdlem10  41336  eupthseg  41374  scmsuppss  41947