Theorem sseq12d 4024

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534   ⊆ wss 3958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2721  df-ss 3975

This theorem is referenced by:  3sstr3d  4037  3sstr4d  4038  sscon34b  4304  ssdifeq0  4492  relcnvtrg  6280  knatar  7372  suppfnss  8208  funsssuppss  8209  csbfrecsg  8303  smogt  8401  oawordri  8584  omwordi  8605  omwordri  8606  oewordi  8625  oewordri  8626  oeworde  8627  nnawordi  8655  nnmwordi  8669  nnmwordri  8670  naddssim  8719  naddss2  8724  sbthlem2  9125  sbth  9134  sbthfi  9240  marypha2lem3  9481  hartogslem1  9586  inf3lem1  9672  dfttrcl2  9768  tcrank  9928  alephle  10132  cfsmolem  10314  isfin3ds  10373  fin23lem17  10382  fin23lem39  10394  isf32lem1  10397  isf32lem2  10398  isf32lem11  10407  isf33lem  10410  isf34lem7  10423  isf34lem6  10424  fin1a2lem13  10456  itunitc1  10464  dominf  10489  dcomex  10491  axdc2lem  10492  dominfac  10617  fpwwe2cbv  10674  fpwwe2lem2  10676  fpwwecbv  10688  fpwwelem  10689  canthwelem  10694  canthwe  10695  wunex2  10782  swrdval  14664  trcleq2lem  15009  dfrtrcl2  15080  vdwpc  16995  vdwlem1  16996  vdwlem6  17001  vdwlem7  17002  vdwlem8  17003  isstruct2  17164  ressval  17258  mreexexlemd  17670  isacs1i  17683  isssc  17849  ssc2  17851  fullfunc  17941  fthfunc  17942  isps  18606  istsr  18621  isdir  18636  gsumvalx  18682  efgi2  19735  dmdprd  20010  dprdss  20041  dmdprdpr  20061  mhpfval  22132  scmatdmat  22508  basis1  22944  baspartn  22948  eltg  22951  cncls  23269  ispnrm  23334  1stcfb  23440  2ndcctbss  23450  1stcelcls  23456  subislly  23476  kgenidm  23542  ptpjpre1  23566  txcmplem2  23637  flimval  23958  flimcf  23977  fclscf  24020  metss  24508  isngp  24596  iscph  25189  cphsscph  25270  equivcau  25319  caubl  25327  caublcls  25328  ovoliunlem3  25524  volsuplem  25575  volsup  25576  dyaddisj  25616  itg1climres  25735  negsbdaylem  28062  isausgr  29097  issubgr  29204  subgrprop3  29209  cusgrfilem1  29389  wkslem1  29541  wkslem2  29542  iswlk  29544  wlkres  29604  redwlk  29606  wlkp1lem8  29614  wlkdlem2  29617  crctcshwlkn0lem4  29744  crctcshwlkn0lem5  29745  crctcshwlkn0lem6  29746  2wlkdlem10  29866  3wlkdlem10  30099  eupthseg  30136  issh  31138  isch  31152  hsupss  31271  shslej  31310  shlub  31344  ledi  31470  pjoi0  31647  mdbr4  32228  dmdbr4  32236  dmdi4  32237  dmdbr5  32238  mdslle1i  32247  mdslle2i  32248  mdslmd1lem1  32255  mdslmd1lem2  32256  mdslmd1lem3  32257  mdslmd1lem4  32258  mdslmd1i  32259  sumdmdlem2  32349  resvval  33218  zhmnrg  33813  ispisys  34016  pfxwlk  34991  cvmliftlem3  35155  ismfs  35417  rdgssun  37125  poimirlem32  37393  volsupnfl  37406  elrefrels2  38256  refreleq  38259  elcnvrefrels2  38272  dfsymrels2  38283  dfsymrel2  38287  elsymrels2  38291  symreleq  38296  elrefsymrels2  38307  dftrrels2  38313  dftrrel2  38315  eltrrels2  38317  trreleq  38320  eleqvrels2  38330  lssatle  38753  pmaple  39500  2polcon4bN  39657  ispautN  39838  diaord  40786  dibord  40898  dihord6apre  40995  dihord3  40996  dihord4  40997  dihcnvord  41013  dvh4dimlem  41182  islpolN  41222  mapdordlem2  41376  mapdcnvordN  41397  mapdindp  41410  hdmaplkr  41652  ismrcd1  42422  ismrcd2  42423  ismrc  42425  incssnn0  42435  diophrw  42483  hbtlem5  42856  hbt  42858  naddgeoa  43128  minregex  43268  minregex2  43269  rclexi  43349  rtrclex  43351  trclubgNEW  43352  rtrclexi  43355  cnvrcl0  43359  cnvtrcl0  43360  dfrtrcl5  43363  trcleq2lemRP  43364  trficl  43403  dfrcl2  43408  relexpss1d  43439  trclrelexplem  43445  brtrclfv2  43461  dfrtrcl3  43467  heeq12  43510  ntrk2imkb  43771  clsk3nimkb  43774  clsk1independent  43780  isotone1  43782  isotone2  43783  ntrclsss  43797  ntrclsiso  43801  ntrclsk2  43802  ntrclsk3  43804  scottabf  43981  ismnu  44002  ismnushort  44042  nzss  44058  iunincfi  44762  fourierdlem89  45882  fourierdlem90  45883  fourierdlem91  45884  meaiuninclem  46167  meaiunincf  46170  meaiuninc3v  46171  meaiuninc3  46172  meaiininclem  46173  meaiininc  46174  caragenss  46191  carageniuncllem1  46208  hoidmvle  46287  ovnhoilem2  46289  hoiqssbl  46312  ovolval5lem2  46340  vonioolem2  46368  vonicclem2  46371  isisubgr  47495  uspgrsprf  47600  scmsuppss  47828