Theorem sseq12d 3969

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sscon34b  4256  ssdifeq0  4439  relcnvtrg  6248  knatar  7335  suppfnss  8162  funsssuppss  8163  csbfrecsg  8258  smogt  8331  oawordri  8512  omwordi  8533  omwordri  8534  oewordi  8554  oewordri  8555  oeworde  8556  nnawordi  8584  nnmwordi  8598  nnmwordri  8599  naddssim  8649  naddss2  8654  sbthlem2  9054  sbth  9063  sbthfi  9161  marypha2lem3  9378  hartogslem1  9485  inf3lem1  9578  dfttrcl2  9674  tcrank  9837  alephle  10039  cfsmolem  10222  isfin3ds  10281  fin23lem17  10290  fin23lem39  10302  isf32lem1  10305  isf32lem2  10306  isf32lem11  10315  isf33lem  10318  isf34lem7  10331  isf34lem6  10332  fin1a2lem13  10364  itunitc1  10372  dominf  10397  dcomex  10399  axdc2lem  10400  dominfac  10526  fpwwe2cbv  10583  fpwwe2lem2  10585  fpwwe2lem4  10587  fpwwecbv  10597  fpwwelem  10598  canthwelem  10603  canthwe  10604  pwfseqlem4  10615  wunex2  10691  swrdval  14652  trcleq2lem  14999  dfrtrcl2  15070  vdwpc  16997  vdwlem1  16998  vdwlem6  17003  vdwlem7  17004  vdwlem8  17005  isstruct2  17166  ressval  17250  mreexexlemd  17657  isacs1i  17670  isssc  17834  ssc2  17836  fullfunc  17922  fthfunc  17923  isps  18581  istsr  18596  isdir  18611  gsumvalx  18691  efgi2  19746  dmdprd  20021  dprdss  20052  dmdprdpr  20072  mhpfval  22181  scmatdmat  22553  basis1  22988  baspartn  22992  eltg  22995  cncls  23312  ispnrm  23377  1stcfb  23483  2ndcctbss  23493  1stcelcls  23499  subislly  23519  kgenidm  23585  ptpjpre1  23609  txcmplem2  23680  flimval  24001  flimcf  24020  fclscf  24063  metss  24546  isngp  24634  iscph  25210  cphsscph  25291  equivcau  25340  caubl  25348  caublcls  25349  ovoliunlem3  25544  volsuplem  25595  volsup  25596  dyaddisj  25636  itg1climres  25754  addbdaylem  28085  addbday  28086  negbdaylem  28124  addonbday  28347  bdaypw2n0bndlem  28531  bdaypw2n0bnd  28532  isausgr  29309  issubgr  29416  subgrprop3  29421  cusgrfilem1  29600  wkslem1  29752  wkslem2  29753  iswlk  29755  wlkres  29813  redwlk  29815  wlkp1lem8  29823  wlkdlem2  29826  crctcshwlkn0lem4  29957  crctcshwlkn0lem5  29958  crctcshwlkn0lem6  29959  2wlkdlem10  30079  3wlkdlem10  30315  eupthseg  30352  issh  31355  isch  31369  hsupss  31488  shslej  31527  shlub  31561  ledi  31687  pjoi0  31864  mdbr4  32445  dmdbr4  32453  dmdi4  32454  dmdbr5  32455  mdslle1i  32464  mdslle2i  32465  mdslmd1lem1  32472  mdslmd1lem2  32473  mdslmd1lem3  32474  mdslmd1lem4  32475  mdslmd1i  32476  sumdmdlem2  32566  resvval  33474  zhmnrg  34221  ispisys  34408  pfxwlk  35427  cvmliftlem3  35590  ismfs  35852  rdgssun  37825  poimirlem32  38104  volsupnfl  38117  elrefrels2  39050  refreleq  39053  elcnvrefrels2  39066  dfsymrels2  39077  dfsymrel2  39085  elsymrels2  39089  symreleq  39094  elrefsymrels2  39105  dftrrels2  39111  dftrrel2  39113  eltrrels2  39115  trreleq  39118  eleqvrels2  39128  lssatle  39592  pmaple  40338  2polcon4bN  40495  ispautN  40676  diaord  41624  dibord  41736  dihord6apre  41833  dihord3  41834  dihord4  41835  dihcnvord  41851  dvh4dimlem  42020  islpolN  42060  mapdordlem2  42214  mapdcnvordN  42235  mapdindp  42248  hdmaplkr  42490  ismrcd1  43232  ismrcd2  43233  ismrc  43235  incssnn0  43245  diophrw  43293  hbtlem5  43658  hbt  43660  naddgeoa  43924  minregex  44063  minregex2  44064  rclexi  44144  rtrclex  44146  trclubgNEW  44147  rtrclexi  44150  cnvrcl0  44154  cnvtrcl0  44155  dfrtrcl5  44158  trcleq2lemRP  44159  trficl  44198  dfrcl2  44203  relexpss1d  44234  trclrelexplem  44240  brtrclfv2  44256  dfrtrcl3  44262  heeq12  44305  ntrk2imkb  44566  clsk3nimkb  44569  clsk1independent  44575  isotone1  44577  isotone2  44578  ntrclsss  44592  ntrclsiso  44596  ntrclsk2  44597  ntrclsk3  44599  scottabf  44769  ismnu  44790  ismnushort  44830  nzss  44846  iunincfi  45625  fourierdlem89  46722  fourierdlem90  46723  fourierdlem91  46724  meaiuninclem  47007  meaiunincf  47010  meaiuninc3v  47011  meaiuninc3  47012  meaiininclem  47013  meaiininc  47014  caragenss  47031  carageniuncllem1  47048  hoidmvle  47127  ovnhoilem2  47129  hoiqssbl  47152  ovolval5lem2  47180  vonioolem2  47208  vonicclem2  47211  isisubgr  48437  uspgrsprf  48721  scmsuppss  48946  setc1onsubc  50176