Theorem sseq12d 3971

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3905

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sscon34b  4257  ssdifeq0  4440  relcnvtrg  6219  knatar  7298  suppfnss  8129  funsssuppss  8130  csbfrecsg  8224  smogt  8297  oawordri  8475  omwordi  8496  omwordri  8497  oewordi  8516  oewordri  8517  oeworde  8518  nnawordi  8546  nnmwordi  8560  nnmwordri  8561  naddssim  8610  naddss2  8615  sbthlem2  9012  sbth  9021  sbthfi  9123  marypha2lem3  9346  hartogslem1  9453  inf3lem1  9543  dfttrcl2  9639  tcrank  9799  alephle  10001  cfsmolem  10183  isfin3ds  10242  fin23lem17  10251  fin23lem39  10263  isf32lem1  10266  isf32lem2  10267  isf32lem11  10276  isf33lem  10279  isf34lem7  10292  isf34lem6  10293  fin1a2lem13  10325  itunitc1  10333  dominf  10358  dcomex  10360  axdc2lem  10361  dominfac  10486  fpwwe2cbv  10543  fpwwe2lem2  10545  fpwwe2lem4  10547  fpwwecbv  10557  fpwwelem  10558  canthwelem  10563  canthwe  10564  pwfseqlem4  10575  wunex2  10651  swrdval  14568  trcleq2lem  14916  dfrtrcl2  14987  vdwpc  16910  vdwlem1  16911  vdwlem6  16916  vdwlem7  16917  vdwlem8  16918  isstruct2  17078  ressval  17162  mreexexlemd  17568  isacs1i  17581  isssc  17745  ssc2  17747  fullfunc  17833  fthfunc  17834  isps  18492  istsr  18507  isdir  18522  gsumvalx  18568  efgi2  19622  dmdprd  19897  dprdss  19928  dmdprdpr  19948  mhpfval  22041  scmatdmat  22418  basis1  22853  baspartn  22857  eltg  22860  cncls  23177  ispnrm  23242  1stcfb  23348  2ndcctbss  23358  1stcelcls  23364  subislly  23384  kgenidm  23450  ptpjpre1  23474  txcmplem2  23545  flimval  23866  flimcf  23885  fclscf  23928  metss  24412  isngp  24500  iscph  25086  cphsscph  25167  equivcau  25216  caubl  25224  caublcls  25225  ovoliunlem3  25421  volsuplem  25472  volsup  25473  dyaddisj  25513  itg1climres  25631  addsbdaylem  27946  addsbday  27947  negsbdaylem  27985  isausgr  29127  issubgr  29234  subgrprop3  29239  cusgrfilem1  29419  wkslem1  29571  wkslem2  29572  iswlk  29574  wlkres  29632  redwlk  29634  wlkp1lem8  29642  wlkdlem2  29645  crctcshwlkn0lem4  29776  crctcshwlkn0lem5  29777  crctcshwlkn0lem6  29778  2wlkdlem10  29898  3wlkdlem10  30131  eupthseg  30168  issh  31170  isch  31184  hsupss  31303  shslej  31342  shlub  31376  ledi  31502  pjoi0  31679  mdbr4  32260  dmdbr4  32268  dmdi4  32269  dmdbr5  32270  mdslle1i  32279  mdslle2i  32280  mdslmd1lem1  32287  mdslmd1lem2  32288  mdslmd1lem3  32289  mdslmd1lem4  32290  mdslmd1i  32291  sumdmdlem2  32381  resvval  33277  zhmnrg  33931  ispisys  34118  pfxwlk  35096  cvmliftlem3  35259  ismfs  35521  rdgssun  37351  poimirlem32  37631  volsupnfl  37644  elrefrels2  38494  refreleq  38497  elcnvrefrels2  38510  dfsymrels2  38521  dfsymrel2  38525  elsymrels2  38529  symreleq  38534  elrefsymrels2  38545  dftrrels2  38551  dftrrel2  38553  eltrrels2  38555  trreleq  38558  eleqvrels2  38568  lssatle  38993  pmaple  39740  2polcon4bN  39897  ispautN  40078  diaord  41026  dibord  41138  dihord6apre  41235  dihord3  41236  dihord4  41237  dihcnvord  41253  dvh4dimlem  41422  islpolN  41462  mapdordlem2  41616  mapdcnvordN  41637  mapdindp  41650  hdmaplkr  41892  ismrcd1  42671  ismrcd2  42672  ismrc  42674  incssnn0  42684  diophrw  42732  hbtlem5  43101  hbt  43103  naddgeoa  43367  minregex  43507  minregex2  43508  rclexi  43588  rtrclex  43590  trclubgNEW  43591  rtrclexi  43594  cnvrcl0  43598  cnvtrcl0  43599  dfrtrcl5  43602  trcleq2lemRP  43603  trficl  43642  dfrcl2  43647  relexpss1d  43678  trclrelexplem  43684  brtrclfv2  43700  dfrtrcl3  43706  heeq12  43749  ntrk2imkb  44010  clsk3nimkb  44013  clsk1independent  44019  isotone1  44021  isotone2  44022  ntrclsss  44036  ntrclsiso  44040  ntrclsk2  44041  ntrclsk3  44043  scottabf  44213  ismnu  44234  ismnushort  44274  nzss  44290  iunincfi  45072  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  meaiuninclem  46462  meaiunincf  46465  meaiuninc3v  46466  meaiuninc3  46467  meaiininclem  46468  meaiininc  46469  caragenss  46486  carageniuncllem1  46503  hoidmvle  46582  ovnhoilem2  46584  hoiqssbl  46607  ovolval5lem2  46635  vonioolem2  46663  vonicclem2  46666  isisubgr  47846  uspgrsprf  48118  scmsuppss  48343  setc1onsubc  49575