Theorem sseq12d 3992

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  sscon34b  4279  ssdifeq0  4462  relcnvtrg  6255  knatar  7350  suppfnss  8188  funsssuppss  8189  csbfrecsg  8283  smogt  8381  oawordri  8562  omwordi  8583  omwordri  8584  oewordi  8603  oewordri  8604  oeworde  8605  nnawordi  8633  nnmwordi  8647  nnmwordri  8648  naddssim  8697  naddss2  8702  sbthlem2  9098  sbth  9107  sbthfi  9213  marypha2lem3  9449  hartogslem1  9556  inf3lem1  9642  dfttrcl2  9738  tcrank  9898  alephle  10102  cfsmolem  10284  isfin3ds  10343  fin23lem17  10352  fin23lem39  10364  isf32lem1  10367  isf32lem2  10368  isf32lem11  10377  isf33lem  10380  isf34lem7  10393  isf34lem6  10394  fin1a2lem13  10426  itunitc1  10434  dominf  10459  dcomex  10461  axdc2lem  10462  dominfac  10587  fpwwe2cbv  10644  fpwwe2lem2  10646  fpwwe2lem4  10648  fpwwecbv  10658  fpwwelem  10659  canthwelem  10664  canthwe  10665  pwfseqlem4  10676  wunex2  10752  swrdval  14661  trcleq2lem  15010  dfrtrcl2  15081  vdwpc  17000  vdwlem1  17001  vdwlem6  17006  vdwlem7  17007  vdwlem8  17008  isstruct2  17168  ressval  17254  mreexexlemd  17656  isacs1i  17669  isssc  17833  ssc2  17835  fullfunc  17921  fthfunc  17922  isps  18578  istsr  18593  isdir  18608  gsumvalx  18654  efgi2  19706  dmdprd  19981  dprdss  20012  dmdprdpr  20032  mhpfval  22076  scmatdmat  22453  basis1  22888  baspartn  22892  eltg  22895  cncls  23212  ispnrm  23277  1stcfb  23383  2ndcctbss  23393  1stcelcls  23399  subislly  23419  kgenidm  23485  ptpjpre1  23509  txcmplem2  23580  flimval  23901  flimcf  23920  fclscf  23963  metss  24447  isngp  24535  iscph  25122  cphsscph  25203  equivcau  25252  caubl  25260  caublcls  25261  ovoliunlem3  25457  volsuplem  25508  volsup  25509  dyaddisj  25549  itg1climres  25667  addsbdaylem  27975  addsbday  27976  negsbdaylem  28014  isausgr  29143  issubgr  29250  subgrprop3  29255  cusgrfilem1  29435  wkslem1  29587  wkslem2  29588  iswlk  29590  wlkres  29650  redwlk  29652  wlkp1lem8  29660  wlkdlem2  29663  crctcshwlkn0lem4  29795  crctcshwlkn0lem5  29796  crctcshwlkn0lem6  29797  2wlkdlem10  29917  3wlkdlem10  30150  eupthseg  30187  issh  31189  isch  31203  hsupss  31322  shslej  31361  shlub  31395  ledi  31521  pjoi0  31698  mdbr4  32279  dmdbr4  32287  dmdi4  32288  dmdbr5  32289  mdslle1i  32298  mdslle2i  32299  mdslmd1lem1  32306  mdslmd1lem2  32307  mdslmd1lem3  32308  mdslmd1lem4  32309  mdslmd1i  32310  sumdmdlem2  32400  resvval  33345  zhmnrg  33996  ispisys  34183  pfxwlk  35146  cvmliftlem3  35309  ismfs  35571  rdgssun  37396  poimirlem32  37676  volsupnfl  37689  elrefrels2  38536  refreleq  38539  elcnvrefrels2  38552  dfsymrels2  38563  dfsymrel2  38567  elsymrels2  38571  symreleq  38576  elrefsymrels2  38587  dftrrels2  38593  dftrrel2  38595  eltrrels2  38597  trreleq  38600  eleqvrels2  38610  lssatle  39033  pmaple  39780  2polcon4bN  39937  ispautN  40118  diaord  41066  dibord  41178  dihord6apre  41275  dihord3  41276  dihord4  41277  dihcnvord  41293  dvh4dimlem  41462  islpolN  41502  mapdordlem2  41656  mapdcnvordN  41677  mapdindp  41690  hdmaplkr  41932  ismrcd1  42721  ismrcd2  42722  ismrc  42724  incssnn0  42734  diophrw  42782  hbtlem5  43152  hbt  43154  naddgeoa  43418  minregex  43558  minregex2  43559  rclexi  43639  rtrclex  43641  trclubgNEW  43642  rtrclexi  43645  cnvrcl0  43649  cnvtrcl0  43650  dfrtrcl5  43653  trcleq2lemRP  43654  trficl  43693  dfrcl2  43698  relexpss1d  43729  trclrelexplem  43735  brtrclfv2  43751  dfrtrcl3  43757  heeq12  43800  ntrk2imkb  44061  clsk3nimkb  44064  clsk1independent  44070  isotone1  44072  isotone2  44073  ntrclsss  44087  ntrclsiso  44091  ntrclsk2  44092  ntrclsk3  44094  scottabf  44264  ismnu  44285  ismnushort  44325  nzss  44341  iunincfi  45118  fourierdlem89  46224  fourierdlem90  46225  fourierdlem91  46226  meaiuninclem  46509  meaiunincf  46512  meaiuninc3v  46513  meaiuninc3  46514  meaiininclem  46515  meaiininc  46516  caragenss  46533  carageniuncllem1  46550  hoidmvle  46629  ovnhoilem2  46631  hoiqssbl  46654  ovolval5lem2  46682  vonioolem2  46710  vonicclem2  46713  isisubgr  47875  uspgrsprf  48121  scmsuppss  48346  setc1onsubc  49479