Theorem sseq12d 3956

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sscon34b  4245  ssdifeq0  4427  relcnvtrg  6223  knatar  7303  suppfnss  8130  funsssuppss  8131  csbfrecsg  8225  smogt  8298  oawordri  8476  omwordi  8497  omwordri  8498  oewordi  8518  oewordri  8519  oeworde  8520  nnawordi  8548  nnmwordi  8562  nnmwordri  8563  naddssim  8612  naddss2  8617  sbthlem2  9017  sbth  9026  sbthfi  9124  marypha2lem3  9341  hartogslem1  9448  inf3lem1  9538  dfttrcl2  9634  tcrank  9797  alephle  9999  cfsmolem  10181  isfin3ds  10240  fin23lem17  10249  fin23lem39  10261  isf32lem1  10264  isf32lem2  10265  isf32lem11  10274  isf33lem  10277  isf34lem7  10290  isf34lem6  10291  fin1a2lem13  10323  itunitc1  10331  dominf  10356  dcomex  10358  axdc2lem  10359  dominfac  10485  fpwwe2cbv  10542  fpwwe2lem2  10544  fpwwe2lem4  10546  fpwwecbv  10556  fpwwelem  10557  canthwelem  10562  canthwe  10563  pwfseqlem4  10574  wunex2  10650  swrdval  14595  trcleq2lem  14942  dfrtrcl2  15013  vdwpc  16940  vdwlem1  16941  vdwlem6  16946  vdwlem7  16947  vdwlem8  16948  isstruct2  17108  ressval  17192  mreexexlemd  17599  isacs1i  17612  isssc  17776  ssc2  17778  fullfunc  17864  fthfunc  17865  isps  18523  istsr  18538  isdir  18553  gsumvalx  18633  efgi2  19689  dmdprd  19964  dprdss  19995  dmdprdpr  20015  mhpfval  22113  scmatdmat  22489  basis1  22924  baspartn  22928  eltg  22931  cncls  23248  ispnrm  23313  1stcfb  23419  2ndcctbss  23429  1stcelcls  23435  subislly  23455  kgenidm  23521  ptpjpre1  23545  txcmplem2  23616  flimval  23937  flimcf  23956  fclscf  23999  metss  24482  isngp  24570  iscph  25146  cphsscph  25227  equivcau  25276  caubl  25284  caublcls  25285  ovoliunlem3  25480  volsuplem  25531  volsup  25532  dyaddisj  25572  itg1climres  25690  addbdaylem  28028  addbday  28029  negbdaylem  28067  addonbday  28290  bdaypw2n0bndlem  28474  bdaypw2n0bnd  28475  isausgr  29252  issubgr  29359  subgrprop3  29364  cusgrfilem1  29544  wkslem1  29696  wkslem2  29697  iswlk  29699  wlkres  29757  redwlk  29759  wlkp1lem8  29767  wlkdlem2  29770  crctcshwlkn0lem4  29901  crctcshwlkn0lem5  29902  crctcshwlkn0lem6  29903  2wlkdlem10  30023  3wlkdlem10  30259  eupthseg  30296  issh  31299  isch  31313  hsupss  31432  shslej  31471  shlub  31505  ledi  31631  pjoi0  31808  mdbr4  32389  dmdbr4  32397  dmdi4  32398  dmdbr5  32399  mdslle1i  32408  mdslle2i  32409  mdslmd1lem1  32416  mdslmd1lem2  32417  mdslmd1lem3  32418  mdslmd1lem4  32419  mdslmd1i  32420  sumdmdlem2  32510  resvval  33409  zhmnrg  34130  ispisys  34317  pfxwlk  35327  cvmliftlem3  35490  ismfs  35752  rdgssun  37705  poimirlem32  37984  volsupnfl  37997  elrefrels2  38930  refreleq  38933  elcnvrefrels2  38946  dfsymrels2  38957  dfsymrel2  38965  elsymrels2  38969  symreleq  38974  elrefsymrels2  38985  dftrrels2  38991  dftrrel2  38993  eltrrels2  38995  trreleq  38998  eleqvrels2  39008  lssatle  39472  pmaple  40218  2polcon4bN  40375  ispautN  40556  diaord  41504  dibord  41616  dihord6apre  41713  dihord3  41714  dihord4  41715  dihcnvord  41731  dvh4dimlem  41900  islpolN  41940  mapdordlem2  42094  mapdcnvordN  42115  mapdindp  42128  hdmaplkr  42370  ismrcd1  43141  ismrcd2  43142  ismrc  43144  incssnn0  43154  diophrw  43202  hbtlem5  43571  hbt  43573  naddgeoa  43837  minregex  43976  minregex2  43977  rclexi  44057  rtrclex  44059  trclubgNEW  44060  rtrclexi  44063  cnvrcl0  44067  cnvtrcl0  44068  dfrtrcl5  44071  trcleq2lemRP  44072  trficl  44111  dfrcl2  44116  relexpss1d  44147  trclrelexplem  44153  brtrclfv2  44169  dfrtrcl3  44175  heeq12  44218  ntrk2imkb  44479  clsk3nimkb  44482  clsk1independent  44488  isotone1  44490  isotone2  44491  ntrclsss  44505  ntrclsiso  44509  ntrclsk2  44510  ntrclsk3  44512  scottabf  44682  ismnu  44703  ismnushort  44743  nzss  44759  iunincfi  45539  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  meaiuninclem  46923  meaiunincf  46926  meaiuninc3v  46927  meaiuninc3  46928  meaiininclem  46929  meaiininc  46930  caragenss  46947  carageniuncllem1  46964  hoidmvle  47043  ovnhoilem2  47045  hoiqssbl  47068  ovolval5lem2  47096  vonioolem2  47124  vonicclem2  47127  isisubgr  48335  uspgrsprf  48619  scmsuppss  48844  setc1onsubc  50074