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  6232  knatar  7312  suppfnss  8139  funsssuppss  8140  csbfrecsg  8234  smogt  8307  oawordri  8485  omwordi  8506  omwordri  8507  oewordi  8527  oewordri  8528  oeworde  8529  nnawordi  8557  nnmwordi  8571  nnmwordri  8572  naddssim  8621  naddss2  8626  sbthlem2  9026  sbth  9035  sbthfi  9133  marypha2lem3  9350  hartogslem1  9457  inf3lem1  9549  dfttrcl2  9645  tcrank  9808  alephle  10010  cfsmolem  10192  isfin3ds  10251  fin23lem17  10260  fin23lem39  10272  isf32lem1  10275  isf32lem2  10276  isf32lem11  10285  isf33lem  10288  isf34lem7  10301  isf34lem6  10302  fin1a2lem13  10334  itunitc1  10342  dominf  10367  dcomex  10369  axdc2lem  10370  dominfac  10496  fpwwe2cbv  10553  fpwwe2lem2  10555  fpwwe2lem4  10557  fpwwecbv  10567  fpwwelem  10568  canthwelem  10573  canthwe  10574  pwfseqlem4  10585  wunex2  10661  swrdval  14606  trcleq2lem  14953  dfrtrcl2  15024  vdwpc  16951  vdwlem1  16952  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  isstruct2  17119  ressval  17203  mreexexlemd  17610  isacs1i  17623  isssc  17787  ssc2  17789  fullfunc  17875  fthfunc  17876  isps  18534  istsr  18549  isdir  18564  gsumvalx  18644  efgi2  19700  dmdprd  19975  dprdss  20006  dmdprdpr  20026  mhpfval  22104  scmatdmat  22480  basis1  22915  baspartn  22919  eltg  22922  cncls  23239  ispnrm  23304  1stcfb  23410  2ndcctbss  23420  1stcelcls  23426  subislly  23446  kgenidm  23512  ptpjpre1  23536  txcmplem2  23607  flimval  23928  flimcf  23947  fclscf  23990  metss  24473  isngp  24561  iscph  25137  cphsscph  25218  equivcau  25267  caubl  25275  caublcls  25276  ovoliunlem3  25471  volsuplem  25522  volsup  25523  dyaddisj  25563  itg1climres  25681  addbdaylem  28009  addbday  28010  negbdaylem  28048  addonbday  28271  bdaypw2n0bndlem  28455  bdaypw2n0bnd  28456  isausgr  29233  issubgr  29340  subgrprop3  29345  cusgrfilem1  29524  wkslem1  29676  wkslem2  29677  iswlk  29679  wlkres  29737  redwlk  29739  wlkp1lem8  29747  wlkdlem2  29750  crctcshwlkn0lem4  29881  crctcshwlkn0lem5  29882  crctcshwlkn0lem6  29883  2wlkdlem10  30003  3wlkdlem10  30239  eupthseg  30276  issh  31279  isch  31293  hsupss  31412  shslej  31451  shlub  31485  ledi  31611  pjoi0  31788  mdbr4  32369  dmdbr4  32377  dmdi4  32378  dmdbr5  32379  mdslle1i  32388  mdslle2i  32389  mdslmd1lem1  32396  mdslmd1lem2  32397  mdslmd1lem3  32398  mdslmd1lem4  32399  mdslmd1i  32400  sumdmdlem2  32490  resvval  33389  zhmnrg  34109  ispisys  34296  pfxwlk  35306  cvmliftlem3  35469  ismfs  35731  rdgssun  37694  poimirlem32  37973  volsupnfl  37986  elrefrels2  38919  refreleq  38922  elcnvrefrels2  38935  dfsymrels2  38946  dfsymrel2  38954  elsymrels2  38958  symreleq  38963  elrefsymrels2  38974  dftrrels2  38980  dftrrel2  38982  eltrrels2  38984  trreleq  38987  eleqvrels2  38997  lssatle  39461  pmaple  40207  2polcon4bN  40364  ispautN  40545  diaord  41493  dibord  41605  dihord6apre  41702  dihord3  41703  dihord4  41704  dihcnvord  41720  dvh4dimlem  41889  islpolN  41929  mapdordlem2  42083  mapdcnvordN  42104  mapdindp  42117  hdmaplkr  42359  ismrcd1  43130  ismrcd2  43131  ismrc  43133  incssnn0  43143  diophrw  43191  hbtlem5  43556  hbt  43558  naddgeoa  43822  minregex  43961  minregex2  43962  rclexi  44042  rtrclex  44044  trclubgNEW  44045  rtrclexi  44048  cnvrcl0  44052  cnvtrcl0  44053  dfrtrcl5  44056  trcleq2lemRP  44057  trficl  44096  dfrcl2  44101  relexpss1d  44132  trclrelexplem  44138  brtrclfv2  44154  dfrtrcl3  44160  heeq12  44203  ntrk2imkb  44464  clsk3nimkb  44467  clsk1independent  44473  isotone1  44475  isotone2  44476  ntrclsss  44490  ntrclsiso  44494  ntrclsk2  44495  ntrclsk3  44497  scottabf  44667  ismnu  44688  ismnushort  44728  nzss  44744  iunincfi  45524  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  meaiuninclem  46908  meaiunincf  46911  meaiuninc3v  46912  meaiuninc3  46913  meaiininclem  46914  meaiininc  46915  caragenss  46932  carageniuncllem1  46949  hoidmvle  47028  ovnhoilem2  47030  hoiqssbl  47053  ovolval5lem2  47081  vonioolem2  47109  vonicclem2  47112  isisubgr  48332  uspgrsprf  48616  scmsuppss  48841  setc1onsubc  50071