Theorem sseq12d 3963

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ⊆ wss 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3915

This theorem is used by:  sscon34b  4249  ssdifeq0  4441  relcnvtrgOLD  6258  sbcfung  6551  knatar  7355  suppfnss  8184  funsssuppss  8185  csbfrecsg  8280  smogt  8353  oawordri  8536  omwordi  8557  omwordri  8558  oewordi  8578  oewordri  8579  oeworde  8580  nnawordi  8608  nnmwordi  8622  nnmwordri  8623  naddssim  8673  naddss2  8678  sbthlem2  9085  sbth  9094  sbthfi  9192  marypha2lem3  9407  hartogslem1  9514  inf3lem1  9607  dfttrcl2  9703  tcrank  9874  scottabf  9911  alephle  10139  cfsmolem  10320  isfin3ds  10379  fin23lem17  10388  fin23lem39  10400  isf32lem1  10403  isf32lem2  10404  isf32lem11  10413  isf33lem  10416  isf34lem7  10429  isf34lem6  10430  fin1a2lem13  10462  itunitc1  10470  dominf  10495  dcomex  10497  axdc2lem  10498  dominfac  10630  fpwwe2cbv  10687  fpwwe2lem2  10689  fpwwe2lem4  10691  fpwwecbv  10701  fpwwelem  10702  canthwelem  10707  canthwe  10708  pwfseqlem4  10719  wunex2  10795  swrdval  14759  trcleq2lem  15112  dfrtrcl2  15183  vdwpc  17120  vdwlem1  17121  vdwlem6  17126  vdwlem7  17127  vdwlem8  17128  isstruct2  17289  ressval  17373  mreexexlemd  17780  isacs1i  17793  isssc  17957  ssc2  17959  fullfunc  18045  fthfunc  18046  isps  18704  istsr  18719  isdir  18734  gsumvalx  18827  efgi2  19901  dmdprd  20176  dprdss  20207  dmdprdpr  20227  mhpfval  22421  scmatdmat  22792  basis1  23230  baspartn  23234  eltg  23237  cncls  23554  ispnrm  23619  1stcfb  23725  2ndcctbss  23736  1stcelcls  23742  subislly  23762  kgenidm  23828  ptpjpre1  23852  txcmplem2  23923  flimval  24244  flimcf  24263  fclscf  24306  metss  24789  isngp  24877  iscph  25453  cphsscph  25534  equivcau  25583  caubl  25591  caublcls  25592  ovoliunlem3  25787  volsuplem  25838  volsup  25839  dyaddisj  25879  itg1climres  25997  addbdaylem  28337  addbday  28338  negbdaylem  28376  addonbday  28599  bdaypw2n0bndlem  28783  bdaypw2n0bnd  28784  isausgr  29679  issubgr  29786  subgrprop3  29791  cusgrfilem1  29970  wkslem1  30122  wkslem2  30123  iswlk  30125  wlkres  30183  redwlk  30185  wlkp1lem8  30193  wlkdlem2  30196  pfxwlk  30200  crctcshwlkn0lem4  30336  crctcshwlkn0lem5  30337  crctcshwlkn0lem6  30338  2wlkdlem10  30458  3wlkdlem10  30704  eupthseg  30741  issh  31744  isch  31758  hsupss  31877  shslej  31916  shlub  31950  ledi  32076  pjoi0  32253  mdbr4  32834  dmdbr4  32842  dmdi4  32843  dmdbr5  32844  mdslle1i  32853  mdslle2i  32854  mdslmd1lem1  32861  mdslmd1lem2  32862  mdslmd1lem3  32863  mdslmd1lem4  32864  mdslmd1i  32865  sumdmdlem2  32955  resvval  33824  zhmnrg  34531  ispisys  34719  cvmliftlem3  35973  ismfs  36235  nmuladdss  36884  rdgssun  38221  poimirlem32  38490  volsupnfl  38503  elrefrels2  39450  refreleq  39453  elcnvrefrels2  39466  dfsymrels2  39477  dfsymrel2  39485  elsymrels2  39489  symreleq  39494  elrefsymrels2  39505  dftrrels2  39511  dftrrel2  39513  eltrrels2  39515  trreleq  39518  eleqvrels2  39528  lssatle  39992  pmaple  40738  2polcon4bN  40895  ispautN  41076  diaord  42024  dibord  42136  dihord6apre  42233  dihord3  42234  dihord4  42235  dihcnvord  42251  dvh4dimlem  42420  islpolN  42460  mapdordlem2  42614  mapdcnvordN  42635  mapdindp  42648  hdmaplkr  42890  ismrcd1  43647  ismrcd2  43648  ismrc  43650  incssnn0  43660  diophrw  43708  hbtlem5  44073  hbt  44075  naddgeoa  44339  minregex  44478  minregex2  44479  rclexi  44559  rtrclex  44561  trclubgNEW  44562  rtrclexi  44565  cnvrcl0  44569  cnvtrcl0  44570  dfrtrcl5  44573  trcleq2lemRP  44574  trficl  44613  dfrcl2  44618  relexpss1d  44649  trclrelexplem  44655  brtrclfv2  44671  dfrtrcl3  44677  heeq12  44720  ntrk2imkb  44981  clsk3nimkb  44984  clsk1independent  44990  isotone1  44992  isotone2  44993  ntrclsss  45007  ntrclsiso  45011  ntrclsk2  45012  ntrclsk3  45014  ismnu  45189  ismnushort  45229  nzss  45245  iunincfi  46030  fourierdlem89  47127  fourierdlem90  47128  fourierdlem91  47129  meaiuninclem  47412  meaiunincf  47415  meaiuninc3v  47416  meaiuninc3  47417  meaiininclem  47418  meaiininc  47419  caragenss  47436  carageniuncllem1  47453  hoidmvle  47532  ovnhoilem2  47534  hoiqssbl  47557  ovolval5lem2  47585  vonioolem2  47613  vonicclem2  47616  isisubgr  48882  uspgrsprf  49166  scmsuppss  49405  setc1onsubc  50632