Theorem sseq12d 4042

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  3sstr3d  4055  3sstr4d  4056  sscon34b  4323  ssdifeq0  4510  relcnvtrg  6297  knatar  7393  suppfnss  8230  funsssuppss  8231  csbfrecsg  8325  smogt  8423  oawordri  8606  omwordi  8627  omwordri  8628  oewordi  8647  oewordri  8648  oeworde  8649  nnawordi  8677  nnmwordi  8691  nnmwordri  8692  naddssim  8741  naddss2  8746  sbthlem2  9150  sbth  9159  sbthfi  9265  marypha2lem3  9506  hartogslem1  9611  inf3lem1  9697  dfttrcl2  9793  tcrank  9953  alephle  10157  cfsmolem  10339  isfin3ds  10398  fin23lem17  10407  fin23lem39  10419  isf32lem1  10422  isf32lem2  10423  isf32lem11  10432  isf33lem  10435  isf34lem7  10448  isf34lem6  10449  fin1a2lem13  10481  itunitc1  10489  dominf  10514  dcomex  10516  axdc2lem  10517  dominfac  10642  fpwwe2cbv  10699  fpwwe2lem2  10701  fpwwe2lem4  10703  fpwwecbv  10713  fpwwelem  10714  canthwelem  10719  canthwe  10720  pwfseqlem4  10731  wunex2  10807  swrdval  14691  trcleq2lem  15040  dfrtrcl2  15111  vdwpc  17027  vdwlem1  17028  vdwlem6  17033  vdwlem7  17034  vdwlem8  17035  isstruct2  17196  ressval  17290  mreexexlemd  17702  isacs1i  17715  isssc  17881  ssc2  17883  fullfunc  17973  fthfunc  17974  isps  18638  istsr  18653  isdir  18668  gsumvalx  18714  efgi2  19767  dmdprd  20042  dprdss  20073  dmdprdpr  20093  mhpfval  22165  scmatdmat  22542  basis1  22978  baspartn  22982  eltg  22985  cncls  23303  ispnrm  23368  1stcfb  23474  2ndcctbss  23484  1stcelcls  23490  subislly  23510  kgenidm  23576  ptpjpre1  23600  txcmplem2  23671  flimval  23992  flimcf  24011  fclscf  24054  metss  24542  isngp  24630  iscph  25223  cphsscph  25304  equivcau  25353  caubl  25361  caublcls  25362  ovoliunlem3  25558  volsuplem  25609  volsup  25610  dyaddisj  25650  itg1climres  25769  addsbdaylem  28067  addsbday  28068  negsbdaylem  28106  isausgr  29199  issubgr  29306  subgrprop3  29311  cusgrfilem1  29491  wkslem1  29643  wkslem2  29644  iswlk  29646  wlkres  29706  redwlk  29708  wlkp1lem8  29716  wlkdlem2  29719  crctcshwlkn0lem4  29846  crctcshwlkn0lem5  29847  crctcshwlkn0lem6  29848  2wlkdlem10  29968  3wlkdlem10  30201  eupthseg  30238  issh  31240  isch  31254  hsupss  31373  shslej  31412  shlub  31446  ledi  31572  pjoi0  31749  mdbr4  32330  dmdbr4  32338  dmdi4  32339  dmdbr5  32340  mdslle1i  32349  mdslle2i  32350  mdslmd1lem1  32357  mdslmd1lem2  32358  mdslmd1lem3  32359  mdslmd1lem4  32360  mdslmd1i  32361  sumdmdlem2  32451  resvval  33318  zhmnrg  33913  ispisys  34116  pfxwlk  35091  cvmliftlem3  35255  ismfs  35517  rdgssun  37344  poimirlem32  37612  volsupnfl  37625  elrefrels2  38474  refreleq  38477  elcnvrefrels2  38490  dfsymrels2  38501  dfsymrel2  38505  elsymrels2  38509  symreleq  38514  elrefsymrels2  38525  dftrrels2  38531  dftrrel2  38533  eltrrels2  38535  trreleq  38538  eleqvrels2  38548  lssatle  38971  pmaple  39718  2polcon4bN  39875  ispautN  40056  diaord  41004  dibord  41116  dihord6apre  41213  dihord3  41214  dihord4  41215  dihcnvord  41231  dvh4dimlem  41400  islpolN  41440  mapdordlem2  41594  mapdcnvordN  41615  mapdindp  41628  hdmaplkr  41870  ismrcd1  42654  ismrcd2  42655  ismrc  42657  incssnn0  42667  diophrw  42715  hbtlem5  43085  hbt  43087  naddgeoa  43356  minregex  43496  minregex2  43497  rclexi  43577  rtrclex  43579  trclubgNEW  43580  rtrclexi  43583  cnvrcl0  43587  cnvtrcl0  43588  dfrtrcl5  43591  trcleq2lemRP  43592  trficl  43631  dfrcl2  43636  relexpss1d  43667  trclrelexplem  43673  brtrclfv2  43689  dfrtrcl3  43695  heeq12  43738  ntrk2imkb  43999  clsk3nimkb  44002  clsk1independent  44008  isotone1  44010  isotone2  44011  ntrclsss  44025  ntrclsiso  44029  ntrclsk2  44030  ntrclsk3  44032  scottabf  44209  ismnu  44230  ismnushort  44270  nzss  44286  iunincfi  44996  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  meaiuninclem  46401  meaiunincf  46404  meaiuninc3v  46405  meaiuninc3  46406  meaiininclem  46407  meaiininc  46408  caragenss  46425  carageniuncllem1  46442  hoidmvle  46521  ovnhoilem2  46523  hoiqssbl  46546  ovolval5lem2  46574  vonioolem2  46602  vonicclem2  46605  isisubgr  47734  uspgrsprf  47869  scmsuppss  48097