Theorem sseq12d 3955

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sscon34b  4239  ssdifeq0  4421  relcnvtrg  6225  knatar  7308  suppfnss  8136  funsssuppss  8137  csbfrecsg  8231  smogt  8304  oawordri  8482  omwordi  8503  omwordri  8504  oewordi  8524  oewordri  8525  oeworde  8526  nnawordi  8554  nnmwordi  8568  nnmwordri  8569  naddssim  8618  naddss2  8623  sbthlem2  9023  sbth  9032  sbthfi  9130  marypha2lem3  9347  hartogslem1  9454  inf3lem1  9547  dfttrcl2  9643  tcrank  9806  alephle  10008  cfsmolem  10190  isfin3ds  10249  fin23lem17  10258  fin23lem39  10270  isf32lem1  10273  isf32lem2  10274  isf32lem11  10283  isf33lem  10286  isf34lem7  10299  isf34lem6  10300  fin1a2lem13  10332  itunitc1  10340  dominf  10365  dcomex  10367  axdc2lem  10368  dominfac  10494  fpwwe2cbv  10551  fpwwe2lem2  10553  fpwwe2lem4  10555  fpwwecbv  10565  fpwwelem  10566  canthwelem  10571  canthwe  10572  pwfseqlem4  10583  wunex2  10659  swrdval  14604  trcleq2lem  14951  dfrtrcl2  15022  vdwpc  16949  vdwlem1  16950  vdwlem6  16955  vdwlem7  16956  vdwlem8  16957  isstruct2  17117  ressval  17201  mreexexlemd  17608  isacs1i  17621  isssc  17785  ssc2  17787  fullfunc  17873  fthfunc  17874  isps  18532  istsr  18547  isdir  18562  gsumvalx  18642  efgi2  19698  dmdprd  19973  dprdss  20004  dmdprdpr  20024  mhpfval  22133  scmatdmat  22505  basis1  22940  baspartn  22944  eltg  22947  cncls  23264  ispnrm  23329  1stcfb  23435  2ndcctbss  23445  1stcelcls  23451  subislly  23471  kgenidm  23537  ptpjpre1  23561  txcmplem2  23632  flimval  23953  flimcf  23972  fclscf  24015  metss  24498  isngp  24586  iscph  25162  cphsscph  25243  equivcau  25292  caubl  25300  caublcls  25301  ovoliunlem3  25496  volsuplem  25547  volsup  25548  dyaddisj  25588  itg1climres  25706  addbdaylem  28034  addbday  28035  negbdaylem  28073  addonbday  28296  bdaypw2n0bndlem  28480  bdaypw2n0bnd  28481  isausgr  29258  issubgr  29365  subgrprop3  29370  cusgrfilem1  29549  wkslem1  29701  wkslem2  29702  iswlk  29704  wlkres  29762  redwlk  29764  wlkp1lem8  29772  wlkdlem2  29775  crctcshwlkn0lem4  29906  crctcshwlkn0lem5  29907  crctcshwlkn0lem6  29908  2wlkdlem10  30028  3wlkdlem10  30264  eupthseg  30301  issh  31304  isch  31318  hsupss  31437  shslej  31476  shlub  31510  ledi  31636  pjoi0  31813  mdbr4  32394  dmdbr4  32402  dmdi4  32403  dmdbr5  32404  mdslle1i  32413  mdslle2i  32414  mdslmd1lem1  32421  mdslmd1lem2  32422  mdslmd1lem3  32423  mdslmd1lem4  32424  mdslmd1i  32425  sumdmdlem2  32515  resvval  33419  zhmnrg  34156  ispisys  34343  pfxwlk  35353  cvmliftlem3  35516  ismfs  35778  rdgssun  37741  poimirlem32  38020  volsupnfl  38033  elrefrels2  38966  refreleq  38969  elcnvrefrels2  38982  dfsymrels2  38993  dfsymrel2  39001  elsymrels2  39005  symreleq  39010  elrefsymrels2  39021  dftrrels2  39027  dftrrel2  39029  eltrrels2  39031  trreleq  39034  eleqvrels2  39044  lssatle  39508  pmaple  40254  2polcon4bN  40411  ispautN  40592  diaord  41540  dibord  41652  dihord6apre  41749  dihord3  41750  dihord4  41751  dihcnvord  41767  dvh4dimlem  41936  islpolN  41976  mapdordlem2  42130  mapdcnvordN  42151  mapdindp  42164  hdmaplkr  42406  ismrcd1  43148  ismrcd2  43149  ismrc  43151  incssnn0  43161  diophrw  43209  hbtlem5  43574  hbt  43576  naddgeoa  43840  minregex  43979  minregex2  43980  rclexi  44060  rtrclex  44062  trclubgNEW  44063  rtrclexi  44066  cnvrcl0  44070  cnvtrcl0  44071  dfrtrcl5  44074  trcleq2lemRP  44075  trficl  44114  dfrcl2  44119  relexpss1d  44150  trclrelexplem  44156  brtrclfv2  44172  dfrtrcl3  44178  heeq12  44221  ntrk2imkb  44482  clsk3nimkb  44485  clsk1independent  44491  isotone1  44493  isotone2  44494  ntrclsss  44508  ntrclsiso  44512  ntrclsk2  44513  ntrclsk3  44515  scottabf  44685  ismnu  44706  ismnushort  44746  nzss  44762  iunincfi  45542  fourierdlem89  46639  fourierdlem90  46640  fourierdlem91  46641  meaiuninclem  46924  meaiunincf  46927  meaiuninc3v  46928  meaiuninc3  46929  meaiininclem  46930  meaiininc  46931  caragenss  46948  carageniuncllem1  46965  hoidmvle  47044  ovnhoilem2  47046  hoiqssbl  47069  ovolval5lem2  47097  vonioolem2  47125  vonicclem2  47128  isisubgr  48354  uspgrsprf  48638  scmsuppss  48863  setc1onsubc  50093