Theorem sseq12d 3969

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1568   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sscon34b  4256  ssdifeq0  4446  relcnvtrg  6268  knatar  7355  suppfnss  8184  funsssuppss  8185  csbfrecsg  8280  smogt  8353  oawordri  8534  omwordi  8555  omwordri  8556  oewordi  8576  oewordri  8577  oeworde  8578  nnawordi  8606  nnmwordi  8620  nnmwordri  8621  naddssim  8671  naddss2  8676  sbthlem2  9075  sbth  9084  sbthfi  9182  marypha2lem3  9396  hartogslem1  9503  inf3lem1  9596  dfttrcl2  9692  tcrank  9855  scottabf  9865  alephle  10071  cfsmolem  10253  isfin3ds  10312  fin23lem17  10321  fin23lem39  10333  isf32lem1  10336  isf32lem2  10337  isf32lem11  10346  isf33lem  10349  isf34lem7  10362  isf34lem6  10363  fin1a2lem13  10395  itunitc1  10403  dominf  10428  dcomex  10430  axdc2lem  10431  dominfac  10557  fpwwe2cbv  10614  fpwwe2lem2  10616  fpwwe2lem4  10618  fpwwecbv  10628  fpwwelem  10629  canthwelem  10634  canthwe  10635  pwfseqlem4  10646  wunex2  10722  swrdval  14681  trcleq2lem  15028  dfrtrcl2  15099  vdwpc  17039  vdwlem1  17040  vdwlem6  17045  vdwlem7  17046  vdwlem8  17047  isstruct2  17208  ressval  17292  mreexexlemd  17699  isacs1i  17712  isssc  17876  ssc2  17878  fullfunc  17964  fthfunc  17965  isps  18623  istsr  18638  isdir  18653  gsumvalx  18733  efgi2  19794  dmdprd  20069  dprdss  20100  dmdprdpr  20120  mhpfval  22280  scmatdmat  22651  basis1  23086  baspartn  23090  eltg  23093  cncls  23410  ispnrm  23475  1stcfb  23581  2ndcctbss  23591  1stcelcls  23597  subislly  23617  kgenidm  23683  ptpjpre1  23707  txcmplem2  23778  flimval  24099  flimcf  24118  fclscf  24161  metss  24644  isngp  24732  iscph  25308  cphsscph  25389  equivcau  25438  caubl  25446  caublcls  25447  ovoliunlem3  25642  volsuplem  25693  volsup  25694  dyaddisj  25734  itg1climres  25852  addbdaylem  28186  addbday  28187  negbdaylem  28225  addonbday  28448  bdaypw2n0bndlem  28632  bdaypw2n0bnd  28633  isausgr  29480  issubgr  29587  subgrprop3  29592  cusgrfilem1  29771  wkslem1  29923  wkslem2  29924  iswlk  29926  wlkres  29984  redwlk  29986  wlkp1lem8  29994  wlkdlem2  29997  crctcshwlkn0lem4  30128  crctcshwlkn0lem5  30129  crctcshwlkn0lem6  30130  2wlkdlem10  30250  3wlkdlem10  30486  eupthseg  30523  issh  31526  isch  31540  hsupss  31659  shslej  31698  shlub  31732  ledi  31858  pjoi0  32035  mdbr4  32616  dmdbr4  32624  dmdi4  32625  dmdbr5  32626  mdslle1i  32635  mdslle2i  32636  mdslmd1lem1  32643  mdslmd1lem2  32644  mdslmd1lem3  32645  mdslmd1lem4  32646  mdslmd1i  32647  sumdmdlem2  32737  resvval  33615  zhmnrg  34321  ispisys  34508  pfxwlk  35582  cvmliftlem3  35745  ismfs  36007  nmuladdss  36656  rdgssun  37990  poimirlem32  38269  volsupnfl  38282  elrefrels2  39215  refreleq  39218  elcnvrefrels2  39231  dfsymrels2  39242  dfsymrel2  39250  elsymrels2  39254  symreleq  39259  elrefsymrels2  39270  dftrrels2  39276  dftrrel2  39278  eltrrels2  39280  trreleq  39283  eleqvrels2  39293  lssatle  39757  pmaple  40503  2polcon4bN  40660  ispautN  40841  diaord  41789  dibord  41901  dihord6apre  41998  dihord3  41999  dihord4  42000  dihcnvord  42016  dvh4dimlem  42185  islpolN  42225  mapdordlem2  42379  mapdcnvordN  42400  mapdindp  42413  hdmaplkr  42655  ismrcd1  43399  ismrcd2  43400  ismrc  43402  incssnn0  43412  diophrw  43460  hbtlem5  43825  hbt  43827  naddgeoa  44091  minregex  44230  minregex2  44231  rclexi  44311  rtrclex  44313  trclubgNEW  44314  rtrclexi  44317  cnvrcl0  44321  cnvtrcl0  44322  dfrtrcl5  44325  trcleq2lemRP  44326  trficl  44365  dfrcl2  44370  relexpss1d  44401  trclrelexplem  44407  brtrclfv2  44423  dfrtrcl3  44429  heeq12  44472  ntrk2imkb  44733  clsk3nimkb  44736  clsk1independent  44742  isotone1  44744  isotone2  44745  ntrclsss  44759  ntrclsiso  44763  ntrclsk2  44764  ntrclsk3  44766  ismnu  44941  ismnushort  44981  nzss  44997  iunincfi  45782  fourierdlem89  46879  fourierdlem90  46880  fourierdlem91  46881  meaiuninclem  47164  meaiunincf  47167  meaiuninc3v  47168  meaiuninc3  47169  meaiininclem  47170  meaiininc  47171  caragenss  47188  carageniuncllem1  47205  hoidmvle  47284  ovnhoilem2  47286  hoiqssbl  47309  ovolval5lem2  47337  vonioolem2  47365  vonicclem2  47368  isisubgr  48594  uspgrsprf  48878  scmsuppss  49118  setc1onsubc  50347