Theorem sseq12d 3968

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3919

This theorem is referenced by:  sscon34b  4257  ssdifeq0  4440  relcnvtrg  6226  knatar  7305  suppfnss  8133  funsssuppss  8134  csbfrecsg  8228  smogt  8301  oawordri  8479  omwordi  8500  omwordri  8501  oewordi  8521  oewordri  8522  oeworde  8523  nnawordi  8551  nnmwordi  8565  nnmwordri  8566  naddssim  8615  naddss2  8620  sbthlem2  9020  sbth  9029  sbthfi  9127  marypha2lem3  9344  hartogslem1  9451  inf3lem1  9541  dfttrcl2  9637  tcrank  9800  alephle  10002  cfsmolem  10184  isfin3ds  10243  fin23lem17  10252  fin23lem39  10264  isf32lem1  10267  isf32lem2  10268  isf32lem11  10277  isf33lem  10280  isf34lem7  10293  isf34lem6  10294  fin1a2lem13  10326  itunitc1  10334  dominf  10359  dcomex  10361  axdc2lem  10362  dominfac  10488  fpwwe2cbv  10545  fpwwe2lem2  10547  fpwwe2lem4  10549  fpwwecbv  10559  fpwwelem  10560  canthwelem  10565  canthwe  10566  pwfseqlem4  10577  wunex2  10653  swrdval  14571  trcleq2lem  14918  dfrtrcl2  14989  vdwpc  16912  vdwlem1  16913  vdwlem6  16918  vdwlem7  16919  vdwlem8  16920  isstruct2  17080  ressval  17164  mreexexlemd  17571  isacs1i  17584  isssc  17748  ssc2  17750  fullfunc  17836  fthfunc  17837  isps  18495  istsr  18510  isdir  18525  gsumvalx  18605  efgi2  19658  dmdprd  19933  dprdss  19964  dmdprdpr  19984  mhpfval  22085  scmatdmat  22463  basis1  22898  baspartn  22902  eltg  22905  cncls  23222  ispnrm  23287  1stcfb  23393  2ndcctbss  23403  1stcelcls  23409  subislly  23429  kgenidm  23495  ptpjpre1  23519  txcmplem2  23590  flimval  23911  flimcf  23930  fclscf  23973  metss  24456  isngp  24544  iscph  25130  cphsscph  25211  equivcau  25260  caubl  25268  caublcls  25269  ovoliunlem3  25465  volsuplem  25516  volsup  25517  dyaddisj  25557  itg1climres  25675  addsbdaylem  27999  addsbday  28000  negsbdaylem  28038  addsonbday  28260  bdaypw2n0sbndlem  28442  bdaypw2n0sbnd  28443  isausgr  29220  issubgr  29327  subgrprop3  29332  cusgrfilem1  29512  wkslem1  29664  wkslem2  29665  iswlk  29667  wlkres  29725  redwlk  29727  wlkp1lem8  29735  wlkdlem2  29738  crctcshwlkn0lem4  29869  crctcshwlkn0lem5  29870  crctcshwlkn0lem6  29871  2wlkdlem10  29991  3wlkdlem10  30227  eupthseg  30264  issh  31266  isch  31280  hsupss  31399  shslej  31438  shlub  31472  ledi  31598  pjoi0  31775  mdbr4  32356  dmdbr4  32364  dmdi4  32365  dmdbr5  32366  mdslle1i  32375  mdslle2i  32376  mdslmd1lem1  32383  mdslmd1lem2  32384  mdslmd1lem3  32385  mdslmd1lem4  32386  mdslmd1i  32387  sumdmdlem2  32477  resvval  33391  zhmnrg  34103  ispisys  34290  pfxwlk  35299  cvmliftlem3  35462  ismfs  35724  rdgssun  37554  poimirlem32  37824  volsupnfl  37837  elrefrels2  38770  refreleq  38773  elcnvrefrels2  38786  dfsymrels2  38797  dfsymrel2  38805  elsymrels2  38809  symreleq  38814  elrefsymrels2  38825  dftrrels2  38831  dftrrel2  38833  eltrrels2  38835  trreleq  38838  eleqvrels2  38848  lssatle  39312  pmaple  40058  2polcon4bN  40215  ispautN  40396  diaord  41344  dibord  41456  dihord6apre  41553  dihord3  41554  dihord4  41555  dihcnvord  41571  dvh4dimlem  41740  islpolN  41780  mapdordlem2  41934  mapdcnvordN  41955  mapdindp  41968  hdmaplkr  42210  ismrcd1  42976  ismrcd2  42977  ismrc  42979  incssnn0  42989  diophrw  43037  hbtlem5  43406  hbt  43408  naddgeoa  43672  minregex  43811  minregex2  43812  rclexi  43892  rtrclex  43894  trclubgNEW  43895  rtrclexi  43898  cnvrcl0  43902  cnvtrcl0  43903  dfrtrcl5  43906  trcleq2lemRP  43907  trficl  43946  dfrcl2  43951  relexpss1d  43982  trclrelexplem  43988  brtrclfv2  44004  dfrtrcl3  44010  heeq12  44053  ntrk2imkb  44314  clsk3nimkb  44317  clsk1independent  44323  isotone1  44325  isotone2  44326  ntrclsss  44340  ntrclsiso  44344  ntrclsk2  44345  ntrclsk3  44347  scottabf  44517  ismnu  44538  ismnushort  44578  nzss  44594  iunincfi  45374  fourierdlem89  46475  fourierdlem90  46476  fourierdlem91  46477  meaiuninclem  46760  meaiunincf  46763  meaiuninc3v  46764  meaiuninc3  46765  meaiininclem  46766  meaiininc  46767  caragenss  46784  carageniuncllem1  46801  hoidmvle  46880  ovnhoilem2  46882  hoiqssbl  46905  ovolval5lem2  46933  vonioolem2  46961  vonicclem2  46964  isisubgr  48144  uspgrsprf  48428  scmsuppss  48653  setc1onsubc  49883