Theorem sseq12d 3965

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3916

This theorem is referenced by:  sscon34b  4255  ssdifeq0  4438  relcnvtrg  6222  knatar  7300  suppfnss  8128  funsssuppss  8129  csbfrecsg  8223  smogt  8296  oawordri  8474  omwordi  8495  omwordri  8496  oewordi  8515  oewordri  8516  oeworde  8517  nnawordi  8545  nnmwordi  8559  nnmwordri  8560  naddssim  8609  naddss2  8614  sbthlem2  9011  sbth  9020  sbthfi  9118  marypha2lem3  9331  hartogslem1  9438  inf3lem1  9528  dfttrcl2  9624  tcrank  9787  alephle  9989  cfsmolem  10171  isfin3ds  10230  fin23lem17  10239  fin23lem39  10251  isf32lem1  10254  isf32lem2  10255  isf32lem11  10264  isf33lem  10267  isf34lem7  10280  isf34lem6  10281  fin1a2lem13  10313  itunitc1  10321  dominf  10346  dcomex  10348  axdc2lem  10349  dominfac  10474  fpwwe2cbv  10531  fpwwe2lem2  10533  fpwwe2lem4  10535  fpwwecbv  10545  fpwwelem  10546  canthwelem  10551  canthwe  10552  pwfseqlem4  10563  wunex2  10639  swrdval  14561  trcleq2lem  14908  dfrtrcl2  14979  vdwpc  16902  vdwlem1  16903  vdwlem6  16908  vdwlem7  16909  vdwlem8  16910  isstruct2  17070  ressval  17154  mreexexlemd  17560  isacs1i  17573  isssc  17737  ssc2  17739  fullfunc  17825  fthfunc  17826  isps  18484  istsr  18499  isdir  18514  gsumvalx  18594  efgi2  19647  dmdprd  19922  dprdss  19953  dmdprdpr  19973  mhpfval  22063  scmatdmat  22440  basis1  22875  baspartn  22879  eltg  22882  cncls  23199  ispnrm  23264  1stcfb  23370  2ndcctbss  23380  1stcelcls  23386  subislly  23406  kgenidm  23472  ptpjpre1  23496  txcmplem2  23567  flimval  23888  flimcf  23907  fclscf  23950  metss  24433  isngp  24521  iscph  25107  cphsscph  25188  equivcau  25237  caubl  25245  caublcls  25246  ovoliunlem3  25442  volsuplem  25493  volsup  25494  dyaddisj  25534  itg1climres  25652  addsbdaylem  27969  addsbday  27970  negsbdaylem  28008  isausgr  29153  issubgr  29260  subgrprop3  29265  cusgrfilem1  29445  wkslem1  29597  wkslem2  29598  iswlk  29600  wlkres  29658  redwlk  29660  wlkp1lem8  29668  wlkdlem2  29671  crctcshwlkn0lem4  29802  crctcshwlkn0lem5  29803  crctcshwlkn0lem6  29804  2wlkdlem10  29924  3wlkdlem10  30160  eupthseg  30197  issh  31199  isch  31213  hsupss  31332  shslej  31371  shlub  31405  ledi  31531  pjoi0  31708  mdbr4  32289  dmdbr4  32297  dmdi4  32298  dmdbr5  32299  mdslle1i  32308  mdslle2i  32309  mdslmd1lem1  32316  mdslmd1lem2  32317  mdslmd1lem3  32318  mdslmd1lem4  32319  mdslmd1i  32320  sumdmdlem2  32410  resvval  33305  zhmnrg  33989  ispisys  34176  pfxwlk  35179  cvmliftlem3  35342  ismfs  35604  rdgssun  37433  poimirlem32  37702  volsupnfl  37715  elrefrels2  38620  refreleq  38623  elcnvrefrels2  38636  dfsymrels2  38647  dfsymrel2  38655  elsymrels2  38659  symreleq  38664  elrefsymrels2  38675  dftrrels2  38681  dftrrel2  38683  eltrrels2  38685  trreleq  38688  eleqvrels2  38698  lssatle  39124  pmaple  39870  2polcon4bN  40027  ispautN  40208  diaord  41156  dibord  41268  dihord6apre  41365  dihord3  41366  dihord4  41367  dihcnvord  41383  dvh4dimlem  41552  islpolN  41592  mapdordlem2  41746  mapdcnvordN  41767  mapdindp  41780  hdmaplkr  42022  ismrcd1  42805  ismrcd2  42806  ismrc  42808  incssnn0  42818  diophrw  42866  hbtlem5  43235  hbt  43237  naddgeoa  43501  minregex  43641  minregex2  43642  rclexi  43722  rtrclex  43724  trclubgNEW  43725  rtrclexi  43728  cnvrcl0  43732  cnvtrcl0  43733  dfrtrcl5  43736  trcleq2lemRP  43737  trficl  43776  dfrcl2  43781  relexpss1d  43812  trclrelexplem  43818  brtrclfv2  43834  dfrtrcl3  43840  heeq12  43883  ntrk2imkb  44144  clsk3nimkb  44147  clsk1independent  44153  isotone1  44155  isotone2  44156  ntrclsss  44170  ntrclsiso  44174  ntrclsk2  44175  ntrclsk3  44177  scottabf  44347  ismnu  44368  ismnushort  44408  nzss  44424  iunincfi  45205  fourierdlem89  46307  fourierdlem90  46308  fourierdlem91  46309  meaiuninclem  46592  meaiunincf  46595  meaiuninc3v  46596  meaiuninc3  46597  meaiininclem  46598  meaiininc  46599  caragenss  46616  carageniuncllem1  46633  hoidmvle  46712  ovnhoilem2  46714  hoiqssbl  46737  ovolval5lem2  46765  vonioolem2  46793  vonicclem2  46796  isisubgr  47976  uspgrsprf  48260  scmsuppss  48485  setc1onsubc  49717