Theorem sseq12d 3892

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507   ⊆ wss 3831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-in 3838  df-ss 3845

This theorem is referenced by:  3sstr3d  3905  3sstr4d  3906  ssdifeq0  4316  relcnvtr  5960  knatar  6935  suppfnss  7660  funsssuppss  7661  smogt  7810  oawordri  7979  omwordi  8000  omwordri  8001  oewordi  8020  oewordri  8021  oeworde  8022  nnawordi  8050  nnmwordi  8064  nnmwordri  8065  sbthlem2  8426  sbth  8435  marypha2lem3  8698  hartogslem1  8803  inf3lem1  8887  tcrank  9109  alephle  9310  cfsmolem  9492  isfin3ds  9551  fin23lem17  9560  fin23lem39  9572  isf32lem1  9575  isf32lem2  9576  isf32lem11  9585  isf33lem  9588  isf34lem7  9601  isf34lem6  9602  fin1a2lem13  9634  itunitc1  9642  dominf  9667  dcomex  9669  axdc2lem  9670  dominfac  9795  fpwwe2cbv  9852  fpwwe2lem2  9854  fpwwecbv  9866  fpwwelem  9867  canthwelem  9872  canthwe  9873  wunex2  9960  swrdval  13809  trcleq2lem  14215  dfrtrcl2  14285  vdwpc  16175  vdwlem1  16176  vdwlem6  16181  vdwlem7  16182  vdwlem8  16183  isstruct2  16352  ressval  16410  mreexexlemd  16776  isacs1i  16789  isssc  16951  ssc2  16953  fullfunc  17037  fthfunc  17038  isps  17673  istsr  17688  isdir  17703  gsumvalx  17741  efgi2  18612  dmdprd  18873  dprdss  18904  dmdprdpr  18924  mhpfval  20041  scmatdmat  20831  basis1  21265  baspartn  21269  eltg  21272  cncls  21589  ispnrm  21654  1stcfb  21760  2ndcctbss  21770  1stcelcls  21776  subislly  21796  kgenidm  21862  ptpjpre1  21886  txcmplem2  21957  flimval  22278  flimcf  22297  fclscf  22340  metss  22824  isngp  22911  iscph  23480  cphsscph  23560  equivcau  23609  caubl  23617  caublcls  23618  ovoliunlem3  23811  volsuplem  23862  volsup  23863  dyaddisj  23903  itg1climres  24021  isausgr  26655  issubgr  26759  subgrprop3  26764  cusgrfilem1  26943  wkslem1  27095  wkslem2  27096  iswlk  27098  wlkres  27159  wlkresOLD  27161  redwlk  27163  wlkp1lem8  27171  wlkdlem2  27174  crctcshwlkn0lem4  27302  crctcshwlkn0lem5  27303  crctcshwlkn0lem6  27304  2wlkdlem10  27444  3wlkdlem10  27701  eupthseg  27738  issh  28767  isch  28781  hsupss  28902  shslej  28941  shlub  28975  ledi  29101  pjoi0  29278  mdbr4  29859  dmdbr4  29867  dmdi4  29868  dmdbr5  29869  mdslle1i  29878  mdslle2i  29879  mdslmd1lem1  29886  mdslmd1lem2  29887  mdslmd1lem3  29888  mdslmd1lem4  29889  mdslmd1i  29890  sumdmdlem2  29980  resvval  30579  zhmnrg  30852  ispisys  31056  cvmliftlem3  32119  ismfs  32316  rdgssun  34101  poimirlem32  34365  volsupnfl  34378  elrefrels2  35202  refreleq  35205  elcnvrefrels2  35215  dfsymrels2  35226  dfsymrel2  35230  elsymrels2  35234  symreleq  35239  elrefsymrels2  35250  dftrrels2  35256  dftrrel2  35258  eltrrels2  35260  trreleq  35263  eleqvrels2  35272  lssatle  35596  pmaple  36342  2polcon4bN  36499  ispautN  36680  diaord  37628  dibord  37740  dihord6apre  37837  dihord3  37838  dihord4  37839  dihcnvord  37855  dvh4dimlem  38024  islpolN  38064  mapdordlem2  38218  mapdcnvordN  38239  mapdindp  38252  hdmaplkr  38494  ismrcd1  38690  ismrcd2  38691  ismrc  38693  incssnn0  38703  diophrw  38751  hbtlem5  39124  hbt  39126  rclexi  39338  rtrclex  39340  trclubgNEW  39341  rtrclexi  39344  cnvrcl0  39348  cnvtrcl0  39349  dfrtrcl5  39352  trcleq2lemRP  39353  trficl  39377  dfrcl2  39382  relexpss1d  39413  trclrelexplem  39419  brtrclfv2  39435  dfrtrcl3  39441  heeq12  39485  sscon34b  39732  ntrk2imkb  39750  clsk3nimkb  39753  clsk1independent  39759  isotone1  39761  isotone2  39762  ntrclsss  39776  ntrclsiso  39780  ntrclsk2  39781  ntrclsk3  39783  scottabf  39951  ismnu  39972  nzss  40065  iunincfi  40782  fourierdlem89  41912  fourierdlem90  41913  fourierdlem91  41914  meaiuninclem  42194  meaiunincf  42197  meaiuninc3v  42198  meaiuninc3  42199  meaiininclem  42200  meaiininc  42201  caragenss  42218  carageniuncllem1  42235  ovnsslelem  42274  hoidmvle  42314  ovnhoilem2  42316  hoiqssbl  42339  ovolval5lem2  42367  ovolval5lem3  42368  vonioolem2  42395  vonicclem2  42398  uspgrsprf  43390  scmsuppss  43787