Theorem sseq12d 3972

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sscon34b  4259  ssdifeq0  4443  relcnvtrg  6258  knatar  7345  suppfnss  8173  funsssuppss  8174  csbfrecsg  8269  smogt  8342  oawordri  8523  omwordi  8544  omwordri  8545  oewordi  8565  oewordri  8566  oeworde  8567  nnawordi  8595  nnmwordi  8609  nnmwordri  8610  naddssim  8660  naddss2  8665  sbthlem2  9064  sbth  9073  sbthfi  9171  marypha2lem3  9385  hartogslem1  9492  inf3lem1  9585  dfttrcl2  9681  tcrank  9844  scottabf  9854  alephle  10060  cfsmolem  10242  isfin3ds  10301  fin23lem17  10310  fin23lem39  10322  isf32lem1  10325  isf32lem2  10326  isf32lem11  10335  isf33lem  10338  isf34lem7  10351  isf34lem6  10352  fin1a2lem13  10384  itunitc1  10392  dominf  10417  dcomex  10419  axdc2lem  10420  dominfac  10546  fpwwe2cbv  10603  fpwwe2lem2  10605  fpwwe2lem4  10607  fpwwecbv  10617  fpwwelem  10618  canthwelem  10623  canthwe  10624  pwfseqlem4  10635  wunex2  10711  swrdval  14671  trcleq2lem  15018  dfrtrcl2  15089  vdwpc  17030  vdwlem1  17031  vdwlem6  17036  vdwlem7  17037  vdwlem8  17038  isstruct2  17199  ressval  17283  mreexexlemd  17690  isacs1i  17703  isssc  17867  ssc2  17869  fullfunc  17955  fthfunc  17956  isps  18614  istsr  18629  isdir  18644  gsumvalx  18724  efgi2  19786  dmdprd  20061  dprdss  20092  dmdprdpr  20112  mhpfval  22261  scmatdmat  22633  basis1  23068  baspartn  23072  eltg  23075  cncls  23392  ispnrm  23457  1stcfb  23563  2ndcctbss  23573  1stcelcls  23579  subislly  23599  kgenidm  23665  ptpjpre1  23689  txcmplem2  23760  flimval  24081  flimcf  24100  fclscf  24143  metss  24626  isngp  24714  iscph  25290  cphsscph  25371  equivcau  25420  caubl  25428  caublcls  25429  ovoliunlem3  25624  volsuplem  25675  volsup  25676  dyaddisj  25716  itg1climres  25834  addbdaylem  28168  addbday  28169  negbdaylem  28207  addonbday  28430  bdaypw2n0bndlem  28614  bdaypw2n0bnd  28615  isausgr  29423  issubgr  29530  subgrprop3  29535  cusgrfilem1  29714  wkslem1  29866  wkslem2  29867  iswlk  29869  wlkres  29927  redwlk  29929  wlkp1lem8  29937  wlkdlem2  29940  crctcshwlkn0lem4  30071  crctcshwlkn0lem5  30072  crctcshwlkn0lem6  30073  2wlkdlem10  30193  3wlkdlem10  30429  eupthseg  30466  issh  31469  isch  31483  hsupss  31602  shslej  31641  shlub  31675  ledi  31801  pjoi0  31978  mdbr4  32559  dmdbr4  32567  dmdi4  32568  dmdbr5  32569  mdslle1i  32578  mdslle2i  32579  mdslmd1lem1  32586  mdslmd1lem2  32587  mdslmd1lem3  32588  mdslmd1lem4  32589  mdslmd1i  32590  sumdmdlem2  32680  resvval  33564  zhmnrg  34272  ispisys  34459  pfxwlk  35487  cvmliftlem3  35650  ismfs  35912  rdgssun  37884  poimirlem32  38163  volsupnfl  38176  elrefrels2  39109  refreleq  39112  elcnvrefrels2  39125  dfsymrels2  39136  dfsymrel2  39144  elsymrels2  39148  symreleq  39153  elrefsymrels2  39164  dftrrels2  39170  dftrrel2  39172  eltrrels2  39174  trreleq  39177  eleqvrels2  39187  lssatle  39651  pmaple  40397  2polcon4bN  40554  ispautN  40735  diaord  41683  dibord  41795  dihord6apre  41892  dihord3  41893  dihord4  41894  dihcnvord  41910  dvh4dimlem  42079  islpolN  42119  mapdordlem2  42273  mapdcnvordN  42294  mapdindp  42307  hdmaplkr  42549  ismrcd1  43291  ismrcd2  43292  ismrc  43294  incssnn0  43304  diophrw  43352  hbtlem5  43717  hbt  43719  naddgeoa  43983  minregex  44122  minregex2  44123  rclexi  44203  rtrclex  44205  trclubgNEW  44206  rtrclexi  44209  cnvrcl0  44213  cnvtrcl0  44214  dfrtrcl5  44217  trcleq2lemRP  44218  trficl  44257  dfrcl2  44262  relexpss1d  44293  trclrelexplem  44299  brtrclfv2  44315  dfrtrcl3  44321  heeq12  44364  ntrk2imkb  44625  clsk3nimkb  44628  clsk1independent  44634  isotone1  44636  isotone2  44637  ntrclsss  44651  ntrclsiso  44655  ntrclsk2  44656  ntrclsk3  44658  ismnu  44835  ismnushort  44875  nzss  44891  iunincfi  45670  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  meaiuninclem  47052  meaiunincf  47055  meaiuninc3v  47056  meaiuninc3  47057  meaiininclem  47058  meaiininc  47059  caragenss  47076  carageniuncllem1  47093  hoidmvle  47172  ovnhoilem2  47174  hoiqssbl  47197  ovolval5lem2  47225  vonioolem2  47253  vonicclem2  47256  isisubgr  48482  uspgrsprf  48766  scmsuppss  49002  setc1onsubc  50231