Theorem sseq12d 4015

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  3sstr3d  4028  3sstr4d  4029  sscon34b  4294  ssdifeq0  4486  relcnvtrg  6263  knatar  7351  suppfnss  8171  funsssuppss  8172  csbfrecsg  8266  smogt  8364  oawordri  8547  omwordi  8568  omwordri  8569  oewordi  8588  oewordri  8589  oeworde  8590  nnawordi  8618  nnmwordi  8632  nnmwordri  8633  naddssim  8681  naddss2  8686  sbthlem2  9081  sbth  9090  sbthfi  9199  marypha2lem3  9429  hartogslem1  9534  inf3lem1  9620  dfttrcl2  9716  tcrank  9876  alephle  10080  cfsmolem  10262  isfin3ds  10321  fin23lem17  10330  fin23lem39  10342  isf32lem1  10345  isf32lem2  10346  isf32lem11  10355  isf33lem  10358  isf34lem7  10371  isf34lem6  10372  fin1a2lem13  10404  itunitc1  10412  dominf  10437  dcomex  10439  axdc2lem  10440  dominfac  10565  fpwwe2cbv  10622  fpwwe2lem2  10624  fpwwecbv  10636  fpwwelem  10637  canthwelem  10642  canthwe  10643  wunex2  10730  swrdval  14590  trcleq2lem  14935  dfrtrcl2  15006  vdwpc  16910  vdwlem1  16911  vdwlem6  16916  vdwlem7  16917  vdwlem8  16918  isstruct2  17079  ressval  17173  mreexexlemd  17585  isacs1i  17598  isssc  17764  ssc2  17766  fullfunc  17854  fthfunc  17855  isps  18518  istsr  18533  isdir  18548  gsumvalx  18592  efgi2  19588  dmdprd  19863  dprdss  19894  dmdprdpr  19914  mhpfval  21674  scmatdmat  22009  basis1  22445  baspartn  22449  eltg  22452  cncls  22770  ispnrm  22835  1stcfb  22941  2ndcctbss  22951  1stcelcls  22957  subislly  22977  kgenidm  23043  ptpjpre1  23067  txcmplem2  23138  flimval  23459  flimcf  23478  fclscf  23521  metss  24009  isngp  24097  iscph  24679  cphsscph  24760  equivcau  24809  caubl  24817  caublcls  24818  ovoliunlem3  25013  volsuplem  25064  volsup  25065  dyaddisj  25105  itg1climres  25224  negsbdaylem  27520  isausgr  28414  issubgr  28518  subgrprop3  28523  cusgrfilem1  28702  wkslem1  28854  wkslem2  28855  iswlk  28857  wlkres  28917  redwlk  28919  wlkp1lem8  28927  wlkdlem2  28930  crctcshwlkn0lem4  29057  crctcshwlkn0lem5  29058  crctcshwlkn0lem6  29059  2wlkdlem10  29179  3wlkdlem10  29412  eupthseg  29449  issh  30449  isch  30463  hsupss  30582  shslej  30621  shlub  30655  ledi  30781  pjoi0  30958  mdbr4  31539  dmdbr4  31547  dmdi4  31548  dmdbr5  31549  mdslle1i  31558  mdslle2i  31559  mdslmd1lem1  31566  mdslmd1lem2  31567  mdslmd1lem3  31568  mdslmd1lem4  31569  mdslmd1i  31570  sumdmdlem2  31660  resvval  32430  zhmnrg  32936  ispisys  33139  pfxwlk  34103  cvmliftlem3  34267  ismfs  34529  rdgssun  36248  poimirlem32  36509  volsupnfl  36522  elrefrels2  37377  refreleq  37380  elcnvrefrels2  37393  dfsymrels2  37404  dfsymrel2  37408  elsymrels2  37412  symreleq  37417  elrefsymrels2  37428  dftrrels2  37434  dftrrel2  37436  eltrrels2  37438  trreleq  37441  eleqvrels2  37451  lssatle  37874  pmaple  38621  2polcon4bN  38778  ispautN  38959  diaord  39907  dibord  40019  dihord6apre  40116  dihord3  40117  dihord4  40118  dihcnvord  40134  dvh4dimlem  40303  islpolN  40343  mapdordlem2  40497  mapdcnvordN  40518  mapdindp  40531  hdmaplkr  40773  ismrcd1  41422  ismrcd2  41423  ismrc  41425  incssnn0  41435  diophrw  41483  hbtlem5  41856  hbt  41858  naddgeoa  42131  minregex  42271  minregex2  42272  rclexi  42352  rtrclex  42354  trclubgNEW  42355  rtrclexi  42358  cnvrcl0  42362  cnvtrcl0  42363  dfrtrcl5  42366  trcleq2lemRP  42367  trficl  42406  dfrcl2  42411  relexpss1d  42442  trclrelexplem  42448  brtrclfv2  42464  dfrtrcl3  42470  heeq12  42513  ntrk2imkb  42774  clsk3nimkb  42777  clsk1independent  42783  isotone1  42785  isotone2  42786  ntrclsss  42800  ntrclsiso  42804  ntrclsk2  42805  ntrclsk3  42807  scottabf  42985  ismnu  43006  ismnushort  43046  nzss  43062  iunincfi  43769  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  meaiuninclem  45183  meaiunincf  45186  meaiuninc3v  45187  meaiuninc3  45188  meaiininclem  45189  meaiininc  45190  caragenss  45207  carageniuncllem1  45224  hoidmvle  45303  ovnhoilem2  45305  hoiqssbl  45328  ovolval5lem2  45356  vonioolem2  45384  vonicclem2  45387  uspgrsprf  46511  scmsuppss  47002