Theorem sseq12d 3983

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  sscon34b  4270  ssdifeq0  4453  relcnvtrg  6242  knatar  7335  suppfnss  8171  funsssuppss  8172  csbfrecsg  8266  smogt  8339  oawordri  8517  omwordi  8538  omwordri  8539  oewordi  8558  oewordri  8559  oeworde  8560  nnawordi  8588  nnmwordi  8602  nnmwordri  8603  naddssim  8652  naddss2  8657  sbthlem2  9058  sbth  9067  sbthfi  9169  marypha2lem3  9395  hartogslem1  9502  inf3lem1  9588  dfttrcl2  9684  tcrank  9844  alephle  10048  cfsmolem  10230  isfin3ds  10289  fin23lem17  10298  fin23lem39  10310  isf32lem1  10313  isf32lem2  10314  isf32lem11  10323  isf33lem  10326  isf34lem7  10339  isf34lem6  10340  fin1a2lem13  10372  itunitc1  10380  dominf  10405  dcomex  10407  axdc2lem  10408  dominfac  10533  fpwwe2cbv  10590  fpwwe2lem2  10592  fpwwe2lem4  10594  fpwwecbv  10604  fpwwelem  10605  canthwelem  10610  canthwe  10611  pwfseqlem4  10622  wunex2  10698  swrdval  14615  trcleq2lem  14964  dfrtrcl2  15035  vdwpc  16958  vdwlem1  16959  vdwlem6  16964  vdwlem7  16965  vdwlem8  16966  isstruct2  17126  ressval  17210  mreexexlemd  17612  isacs1i  17625  isssc  17789  ssc2  17791  fullfunc  17877  fthfunc  17878  isps  18534  istsr  18549  isdir  18564  gsumvalx  18610  efgi2  19662  dmdprd  19937  dprdss  19968  dmdprdpr  19988  mhpfval  22032  scmatdmat  22409  basis1  22844  baspartn  22848  eltg  22851  cncls  23168  ispnrm  23233  1stcfb  23339  2ndcctbss  23349  1stcelcls  23355  subislly  23375  kgenidm  23441  ptpjpre1  23465  txcmplem2  23536  flimval  23857  flimcf  23876  fclscf  23919  metss  24403  isngp  24491  iscph  25077  cphsscph  25158  equivcau  25207  caubl  25215  caublcls  25216  ovoliunlem3  25412  volsuplem  25463  volsup  25464  dyaddisj  25504  itg1climres  25622  addsbdaylem  27930  addsbday  27931  negsbdaylem  27969  isausgr  29098  issubgr  29205  subgrprop3  29210  cusgrfilem1  29390  wkslem1  29542  wkslem2  29543  iswlk  29545  wlkres  29605  redwlk  29607  wlkp1lem8  29615  wlkdlem2  29618  crctcshwlkn0lem4  29750  crctcshwlkn0lem5  29751  crctcshwlkn0lem6  29752  2wlkdlem10  29872  3wlkdlem10  30105  eupthseg  30142  issh  31144  isch  31158  hsupss  31277  shslej  31316  shlub  31350  ledi  31476  pjoi0  31653  mdbr4  32234  dmdbr4  32242  dmdi4  32243  dmdbr5  32244  mdslle1i  32253  mdslle2i  32254  mdslmd1lem1  32261  mdslmd1lem2  32262  mdslmd1lem3  32263  mdslmd1lem4  32264  mdslmd1i  32265  sumdmdlem2  32355  resvval  33308  zhmnrg  33962  ispisys  34149  pfxwlk  35118  cvmliftlem3  35281  ismfs  35543  rdgssun  37373  poimirlem32  37653  volsupnfl  37666  elrefrels2  38516  refreleq  38519  elcnvrefrels2  38532  dfsymrels2  38543  dfsymrel2  38547  elsymrels2  38551  symreleq  38556  elrefsymrels2  38567  dftrrels2  38573  dftrrel2  38575  eltrrels2  38577  trreleq  38580  eleqvrels2  38590  lssatle  39015  pmaple  39762  2polcon4bN  39919  ispautN  40100  diaord  41048  dibord  41160  dihord6apre  41257  dihord3  41258  dihord4  41259  dihcnvord  41275  dvh4dimlem  41444  islpolN  41484  mapdordlem2  41638  mapdcnvordN  41659  mapdindp  41672  hdmaplkr  41914  ismrcd1  42693  ismrcd2  42694  ismrc  42696  incssnn0  42706  diophrw  42754  hbtlem5  43124  hbt  43126  naddgeoa  43390  minregex  43530  minregex2  43531  rclexi  43611  rtrclex  43613  trclubgNEW  43614  rtrclexi  43617  cnvrcl0  43621  cnvtrcl0  43622  dfrtrcl5  43625  trcleq2lemRP  43626  trficl  43665  dfrcl2  43670  relexpss1d  43701  trclrelexplem  43707  brtrclfv2  43723  dfrtrcl3  43729  heeq12  43772  ntrk2imkb  44033  clsk3nimkb  44036  clsk1independent  44042  isotone1  44044  isotone2  44045  ntrclsss  44059  ntrclsiso  44063  ntrclsk2  44064  ntrclsk3  44066  scottabf  44236  ismnu  44257  ismnushort  44297  nzss  44313  iunincfi  45095  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  meaiuninclem  46485  meaiunincf  46488  meaiuninc3v  46489  meaiuninc3  46490  meaiininclem  46491  meaiininc  46492  caragenss  46509  carageniuncllem1  46526  hoidmvle  46605  ovnhoilem2  46607  hoiqssbl  46630  ovolval5lem2  46658  vonioolem2  46686  vonicclem2  46689  isisubgr  47866  uspgrsprf  48138  scmsuppss  48363  setc1onsubc  49595