Theorem sseq12d 3966

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2722  df-ss 3917

This theorem is referenced by:  sscon34b  4252  ssdifeq0  4435  relcnvtrg  6210  knatar  7286  suppfnss  8114  funsssuppss  8115  csbfrecsg  8209  smogt  8282  oawordri  8460  omwordi  8481  omwordri  8482  oewordi  8501  oewordri  8502  oeworde  8503  nnawordi  8531  nnmwordi  8545  nnmwordri  8546  naddssim  8595  naddss2  8600  sbthlem2  8996  sbth  9005  sbthfi  9103  marypha2lem3  9316  hartogslem1  9423  inf3lem1  9513  dfttrcl2  9609  tcrank  9769  alephle  9971  cfsmolem  10153  isfin3ds  10212  fin23lem17  10221  fin23lem39  10233  isf32lem1  10236  isf32lem2  10237  isf32lem11  10246  isf33lem  10249  isf34lem7  10262  isf34lem6  10263  fin1a2lem13  10295  itunitc1  10303  dominf  10328  dcomex  10330  axdc2lem  10331  dominfac  10456  fpwwe2cbv  10513  fpwwe2lem2  10515  fpwwe2lem4  10517  fpwwecbv  10527  fpwwelem  10528  canthwelem  10533  canthwe  10534  pwfseqlem4  10545  wunex2  10621  swrdval  14543  trcleq2lem  14890  dfrtrcl2  14961  vdwpc  16884  vdwlem1  16885  vdwlem6  16890  vdwlem7  16891  vdwlem8  16892  isstruct2  17052  ressval  17136  mreexexlemd  17542  isacs1i  17555  isssc  17719  ssc2  17721  fullfunc  17807  fthfunc  17808  isps  18466  istsr  18481  isdir  18496  gsumvalx  18576  efgi2  19630  dmdprd  19905  dprdss  19936  dmdprdpr  19956  mhpfval  22046  scmatdmat  22423  basis1  22858  baspartn  22862  eltg  22865  cncls  23182  ispnrm  23247  1stcfb  23353  2ndcctbss  23363  1stcelcls  23369  subislly  23389  kgenidm  23455  ptpjpre1  23479  txcmplem2  23550  flimval  23871  flimcf  23890  fclscf  23933  metss  24416  isngp  24504  iscph  25090  cphsscph  25171  equivcau  25220  caubl  25228  caublcls  25229  ovoliunlem3  25425  volsuplem  25476  volsup  25477  dyaddisj  25517  itg1climres  25635  addsbdaylem  27952  addsbday  27953  negsbdaylem  27991  isausgr  29135  issubgr  29242  subgrprop3  29247  cusgrfilem1  29427  wkslem1  29579  wkslem2  29580  iswlk  29582  wlkres  29640  redwlk  29642  wlkp1lem8  29650  wlkdlem2  29653  crctcshwlkn0lem4  29784  crctcshwlkn0lem5  29785  crctcshwlkn0lem6  29786  2wlkdlem10  29906  3wlkdlem10  30139  eupthseg  30176  issh  31178  isch  31192  hsupss  31311  shslej  31350  shlub  31384  ledi  31510  pjoi0  31687  mdbr4  32268  dmdbr4  32276  dmdi4  32277  dmdbr5  32278  mdslle1i  32287  mdslle2i  32288  mdslmd1lem1  32295  mdslmd1lem2  32296  mdslmd1lem3  32297  mdslmd1lem4  32298  mdslmd1i  32299  sumdmdlem2  32389  resvval  33284  zhmnrg  33968  ispisys  34155  pfxwlk  35136  cvmliftlem3  35299  ismfs  35561  rdgssun  37391  poimirlem32  37671  volsupnfl  37684  elrefrels2  38534  refreleq  38537  elcnvrefrels2  38550  dfsymrels2  38561  dfsymrel2  38565  elsymrels2  38569  symreleq  38574  elrefsymrels2  38585  dftrrels2  38591  dftrrel2  38593  eltrrels2  38595  trreleq  38598  eleqvrels2  38608  lssatle  39033  pmaple  39779  2polcon4bN  39936  ispautN  40117  diaord  41065  dibord  41177  dihord6apre  41274  dihord3  41275  dihord4  41276  dihcnvord  41292  dvh4dimlem  41461  islpolN  41501  mapdordlem2  41655  mapdcnvordN  41676  mapdindp  41689  hdmaplkr  41931  ismrcd1  42710  ismrcd2  42711  ismrc  42713  incssnn0  42723  diophrw  42771  hbtlem5  43140  hbt  43142  naddgeoa  43406  minregex  43546  minregex2  43547  rclexi  43627  rtrclex  43629  trclubgNEW  43630  rtrclexi  43633  cnvrcl0  43637  cnvtrcl0  43638  dfrtrcl5  43641  trcleq2lemRP  43642  trficl  43681  dfrcl2  43686  relexpss1d  43717  trclrelexplem  43723  brtrclfv2  43739  dfrtrcl3  43745  heeq12  43788  ntrk2imkb  44049  clsk3nimkb  44052  clsk1independent  44058  isotone1  44060  isotone2  44061  ntrclsss  44075  ntrclsiso  44079  ntrclsk2  44080  ntrclsk3  44082  scottabf  44252  ismnu  44273  ismnushort  44313  nzss  44329  iunincfi  45110  fourierdlem89  46212  fourierdlem90  46213  fourierdlem91  46214  meaiuninclem  46497  meaiunincf  46500  meaiuninc3v  46501  meaiuninc3  46502  meaiininclem  46503  meaiininc  46504  caragenss  46521  carageniuncllem1  46538  hoidmvle  46617  ovnhoilem2  46619  hoiqssbl  46642  ovolval5lem2  46670  vonioolem2  46698  vonicclem2  46701  isisubgr  47872  uspgrsprf  48156  scmsuppss  48381  setc1onsubc  49613