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 278	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540   ⊆ wss 3898

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  3sstr3d  3978  3sstr4d  3979  sscon34b  4241  ssdifeq0  4431  relcnvtrg  6204  knatar  7284  suppfnss  8075  funsssuppss  8076  csbfrecsg  8170  smogt  8268  oawordri  8452  omwordi  8473  omwordri  8474  oewordi  8493  oewordri  8494  oeworde  8495  nnawordi  8523  nnmwordi  8537  nnmwordri  8538  sbthlem2  8949  sbth  8958  sbthfi  9067  marypha2lem3  9294  hartogslem1  9399  inf3lem1  9485  dfttrcl2  9581  tcrank  9741  alephle  9945  cfsmolem  10127  isfin3ds  10186  fin23lem17  10195  fin23lem39  10207  isf32lem1  10210  isf32lem2  10211  isf32lem11  10220  isf33lem  10223  isf34lem7  10236  isf34lem6  10237  fin1a2lem13  10269  itunitc1  10277  dominf  10302  dcomex  10304  axdc2lem  10305  dominfac  10430  fpwwe2cbv  10487  fpwwe2lem2  10489  fpwwecbv  10501  fpwwelem  10502  canthwelem  10507  canthwe  10508  wunex2  10595  swrdval  14454  trcleq2lem  14801  dfrtrcl2  14872  vdwpc  16778  vdwlem1  16779  vdwlem6  16784  vdwlem7  16785  vdwlem8  16786  isstruct2  16947  ressval  17041  mreexexlemd  17450  isacs1i  17463  isssc  17629  ssc2  17631  fullfunc  17719  fthfunc  17720  isps  18383  istsr  18398  isdir  18413  gsumvalx  18457  efgi2  19426  dmdprd  19696  dprdss  19727  dmdprdpr  19747  mhpfval  21435  scmatdmat  21770  basis1  22206  baspartn  22210  eltg  22213  cncls  22531  ispnrm  22596  1stcfb  22702  2ndcctbss  22712  1stcelcls  22718  subislly  22738  kgenidm  22804  ptpjpre1  22828  txcmplem2  22899  flimval  23220  flimcf  23239  fclscf  23282  metss  23770  isngp  23858  iscph  24440  cphsscph  24521  equivcau  24570  caubl  24578  caublcls  24579  ovoliunlem3  24774  volsuplem  24825  volsup  24826  dyaddisj  24866  itg1climres  24985  isausgr  27823  issubgr  27927  subgrprop3  27932  cusgrfilem1  28111  wkslem1  28263  wkslem2  28264  iswlk  28266  wlkres  28326  redwlk  28328  wlkp1lem8  28336  wlkdlem2  28339  crctcshwlkn0lem4  28466  crctcshwlkn0lem5  28467  crctcshwlkn0lem6  28468  2wlkdlem10  28588  3wlkdlem10  28821  eupthseg  28858  issh  29858  isch  29872  hsupss  29991  shslej  30030  shlub  30064  ledi  30190  pjoi0  30367  mdbr4  30948  dmdbr4  30956  dmdi4  30957  dmdbr5  30958  mdslle1i  30967  mdslle2i  30968  mdslmd1lem1  30975  mdslmd1lem2  30976  mdslmd1lem3  30977  mdslmd1lem4  30978  mdslmd1i  30979  sumdmdlem2  31069  resvval  31822  zhmnrg  32215  ispisys  32418  pfxwlk  33384  cvmliftlem3  33548  ismfs  33810  naddssim  34116  naddss2  34121  rdgssun  35662  poimirlem32  35922  volsupnfl  35935  elrefrels2  36793  refreleq  36796  elcnvrefrels2  36809  dfsymrels2  36820  dfsymrel2  36824  elsymrels2  36828  symreleq  36833  elrefsymrels2  36844  dftrrels2  36850  dftrrel2  36852  eltrrels2  36854  trreleq  36857  eleqvrels2  36867  lssatle  37290  pmaple  38037  2polcon4bN  38194  ispautN  38375  diaord  39323  dibord  39435  dihord6apre  39532  dihord3  39533  dihord4  39534  dihcnvord  39550  dvh4dimlem  39719  islpolN  39759  mapdordlem2  39913  mapdcnvordN  39934  mapdindp  39947  hdmaplkr  40189  ismrcd1  40790  ismrcd2  40791  ismrc  40793  incssnn0  40803  diophrw  40851  hbtlem5  41224  hbt  41226  minregex  41471  minregex2  41472  rclexi  41552  rtrclex  41554  trclubgNEW  41555  rtrclexi  41558  cnvrcl0  41562  cnvtrcl0  41563  dfrtrcl5  41566  trcleq2lemRP  41567  trficl  41606  dfrcl2  41611  relexpss1d  41642  trclrelexplem  41648  brtrclfv2  41664  dfrtrcl3  41670  heeq12  41713  ntrk2imkb  41976  clsk3nimkb  41979  clsk1independent  41985  isotone1  41987  isotone2  41988  ntrclsss  42002  ntrclsiso  42006  ntrclsk2  42007  ntrclsk3  42009  scottabf  42187  ismnu  42208  ismnushort  42248  nzss  42264  iunincfi  42972  fourierdlem89  44080  fourierdlem90  44081  fourierdlem91  44082  meaiuninclem  44363  meaiunincf  44366  meaiuninc3v  44367  meaiuninc3  44368  meaiininclem  44369  meaiininc  44370  caragenss  44387  carageniuncllem1  44404  hoidmvle  44483  ovnhoilem2  44485  hoiqssbl  44508  ovolval5lem2  44536  vonioolem2  44564  vonicclem2  44567  uspgrsprf  45667  scmsuppss  46067