Theorem sseq12d 4014

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  3sstr3d  4027  3sstr4d  4028  sscon34b  4293  ssdifeq0  4485  relcnvtrg  6264  knatar  7356  suppfnss  8176  funsssuppss  8177  csbfrecsg  8271  smogt  8369  oawordri  8552  omwordi  8573  omwordri  8574  oewordi  8593  oewordri  8594  oeworde  8595  nnawordi  8623  nnmwordi  8637  nnmwordri  8638  naddssim  8686  naddss2  8691  sbthlem2  9086  sbth  9095  sbthfi  9204  marypha2lem3  9434  hartogslem1  9539  inf3lem1  9625  dfttrcl2  9721  tcrank  9881  alephle  10085  cfsmolem  10267  isfin3ds  10326  fin23lem17  10335  fin23lem39  10347  isf32lem1  10350  isf32lem2  10351  isf32lem11  10360  isf33lem  10363  isf34lem7  10376  isf34lem6  10377  fin1a2lem13  10409  itunitc1  10417  dominf  10442  dcomex  10444  axdc2lem  10445  dominfac  10570  fpwwe2cbv  10627  fpwwe2lem2  10629  fpwwecbv  10641  fpwwelem  10642  canthwelem  10647  canthwe  10648  wunex2  10735  swrdval  14597  trcleq2lem  14942  dfrtrcl2  15013  vdwpc  16917  vdwlem1  16918  vdwlem6  16923  vdwlem7  16924  vdwlem8  16925  isstruct2  17086  ressval  17180  mreexexlemd  17592  isacs1i  17605  isssc  17771  ssc2  17773  fullfunc  17861  fthfunc  17862  isps  18525  istsr  18540  isdir  18555  gsumvalx  18601  efgi2  19634  dmdprd  19909  dprdss  19940  dmdprdpr  19960  mhpfval  21901  scmatdmat  22237  basis1  22673  baspartn  22677  eltg  22680  cncls  22998  ispnrm  23063  1stcfb  23169  2ndcctbss  23179  1stcelcls  23185  subislly  23205  kgenidm  23271  ptpjpre1  23295  txcmplem2  23366  flimval  23687  flimcf  23706  fclscf  23749  metss  24237  isngp  24325  iscph  24918  cphsscph  24999  equivcau  25048  caubl  25056  caublcls  25057  ovoliunlem3  25253  volsuplem  25304  volsup  25305  dyaddisj  25345  itg1climres  25464  negsbdaylem  27769  isausgr  28691  issubgr  28795  subgrprop3  28800  cusgrfilem1  28979  wkslem1  29131  wkslem2  29132  iswlk  29134  wlkres  29194  redwlk  29196  wlkp1lem8  29204  wlkdlem2  29207  crctcshwlkn0lem4  29334  crctcshwlkn0lem5  29335  crctcshwlkn0lem6  29336  2wlkdlem10  29456  3wlkdlem10  29689  eupthseg  29726  issh  30728  isch  30742  hsupss  30861  shslej  30900  shlub  30934  ledi  31060  pjoi0  31237  mdbr4  31818  dmdbr4  31826  dmdi4  31827  dmdbr5  31828  mdslle1i  31837  mdslle2i  31838  mdslmd1lem1  31845  mdslmd1lem2  31846  mdslmd1lem3  31847  mdslmd1lem4  31848  mdslmd1i  31849  sumdmdlem2  31939  resvval  32711  zhmnrg  33245  ispisys  33448  pfxwlk  34412  cvmliftlem3  34576  ismfs  34838  rdgssun  36562  poimirlem32  36823  volsupnfl  36836  elrefrels2  37691  refreleq  37694  elcnvrefrels2  37707  dfsymrels2  37718  dfsymrel2  37722  elsymrels2  37726  symreleq  37731  elrefsymrels2  37742  dftrrels2  37748  dftrrel2  37750  eltrrels2  37752  trreleq  37755  eleqvrels2  37765  lssatle  38188  pmaple  38935  2polcon4bN  39092  ispautN  39273  diaord  40221  dibord  40333  dihord6apre  40430  dihord3  40431  dihord4  40432  dihcnvord  40448  dvh4dimlem  40617  islpolN  40657  mapdordlem2  40811  mapdcnvordN  40832  mapdindp  40845  hdmaplkr  41087  ismrcd1  41738  ismrcd2  41739  ismrc  41741  incssnn0  41751  diophrw  41799  hbtlem5  42172  hbt  42174  naddgeoa  42447  minregex  42587  minregex2  42588  rclexi  42668  rtrclex  42670  trclubgNEW  42671  rtrclexi  42674  cnvrcl0  42678  cnvtrcl0  42679  dfrtrcl5  42682  trcleq2lemRP  42683  trficl  42722  dfrcl2  42727  relexpss1d  42758  trclrelexplem  42764  brtrclfv2  42780  dfrtrcl3  42786  heeq12  42829  ntrk2imkb  43090  clsk3nimkb  43093  clsk1independent  43099  isotone1  43101  isotone2  43102  ntrclsss  43116  ntrclsiso  43120  ntrclsk2  43121  ntrclsk3  43123  scottabf  43301  ismnu  43322  ismnushort  43362  nzss  43378  iunincfi  44084  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  meaiuninclem  45494  meaiunincf  45497  meaiuninc3v  45498  meaiuninc3  45499  meaiininclem  45500  meaiininc  45501  caragenss  45518  carageniuncllem1  45535  hoidmvle  45614  ovnhoilem2  45616  hoiqssbl  45639  ovolval5lem2  45667  vonioolem2  45695  vonicclem2  45698  uspgrsprf  46822  scmsuppss  47136