Theorem sseq12d 3973

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  sscon34b  4260  ssdifeq0  4452  relcnvtrgOLD  6274  knatar  7368  suppfnss  8194  funsssuppss  8195  csbfrecsg  8290  smogt  8363  oawordri  8544  omwordi  8565  omwordri  8566  oewordi  8586  oewordri  8587  oeworde  8588  nnawordi  8616  nnmwordi  8630  nnmwordri  8631  naddssim  8681  naddss2  8686  sbthlem2  9086  sbth  9095  sbthfi  9193  marypha2lem3  9407  hartogslem1  9514  inf3lem1  9607  dfttrcl2  9703  tcrank  9866  scottabf  9878  alephle  10091  cfsmolem  10272  isfin3ds  10331  fin23lem17  10340  fin23lem39  10352  isf32lem1  10355  isf32lem2  10356  isf32lem11  10365  isf33lem  10368  isf34lem7  10381  isf34lem6  10382  fin1a2lem13  10414  itunitc1  10422  dominf  10447  dcomex  10449  axdc2lem  10450  dominfac  10576  fpwwe2cbv  10633  fpwwe2lem2  10635  fpwwe2lem4  10637  fpwwecbv  10647  fpwwelem  10648  canthwelem  10653  canthwe  10654  pwfseqlem4  10665  wunex2  10741  swrdval  14703  trcleq2lem  15054  dfrtrcl2  15125  vdwpc  17065  vdwlem1  17066  vdwlem6  17071  vdwlem7  17072  vdwlem8  17073  isstruct2  17234  ressval  17318  mreexexlemd  17725  isacs1i  17738  isssc  17902  ssc2  17904  fullfunc  17990  fthfunc  17991  isps  18649  istsr  18664  isdir  18679  gsumvalx  18759  efgi2  19820  dmdprd  20095  dprdss  20126  dmdprdpr  20146  mhpfval  22331  scmatdmat  22702  basis1  23137  baspartn  23141  eltg  23144  cncls  23461  ispnrm  23526  1stcfb  23632  2ndcctbss  23642  1stcelcls  23648  subislly  23668  kgenidm  23734  ptpjpre1  23758  txcmplem2  23829  flimval  24150  flimcf  24169  fclscf  24212  metss  24695  isngp  24783  iscph  25359  cphsscph  25440  equivcau  25489  caubl  25497  caublcls  25498  ovoliunlem3  25693  volsuplem  25744  volsup  25745  dyaddisj  25785  itg1climres  25903  addbdaylem  28240  addbday  28241  negbdaylem  28279  addonbday  28502  bdaypw2n0bndlem  28686  bdaypw2n0bnd  28687  isausgr  29544  issubgr  29651  subgrprop3  29656  cusgrfilem1  29835  wkslem1  29987  wkslem2  29988  iswlk  29990  wlkres  30048  redwlk  30050  wlkp1lem8  30058  wlkdlem2  30061  crctcshwlkn0lem4  30192  crctcshwlkn0lem5  30193  crctcshwlkn0lem6  30194  2wlkdlem10  30314  3wlkdlem10  30550  eupthseg  30587  issh  31590  isch  31604  hsupss  31723  shslej  31762  shlub  31796  ledi  31922  pjoi0  32099  mdbr4  32680  dmdbr4  32688  dmdi4  32689  dmdbr5  32690  mdslle1i  32699  mdslle2i  32700  mdslmd1lem1  32707  mdslmd1lem2  32708  mdslmd1lem3  32709  mdslmd1lem4  32710  mdslmd1i  32711  sumdmdlem2  32801  resvval  33673  zhmnrg  34379  ispisys  34566  pfxwlk  35629  cvmliftlem3  35792  ismfs  36054  nmuladdss  36718  rdgssun  38057  poimirlem32  38336  volsupnfl  38349  elrefrels2  39280  refreleq  39283  elcnvrefrels2  39296  dfsymrels2  39307  dfsymrel2  39315  elsymrels2  39319  symreleq  39324  elrefsymrels2  39335  dftrrels2  39341  dftrrel2  39343  eltrrels2  39345  trreleq  39348  eleqvrels2  39358  lssatle  39822  pmaple  40568  2polcon4bN  40725  ispautN  40906  diaord  41854  dibord  41966  dihord6apre  42063  dihord3  42064  dihord4  42065  dihcnvord  42081  dvh4dimlem  42250  islpolN  42290  mapdordlem2  42444  mapdcnvordN  42465  mapdindp  42478  hdmaplkr  42720  ismrcd1  43462  ismrcd2  43463  ismrc  43465  incssnn0  43475  diophrw  43523  hbtlem5  43888  hbt  43890  naddgeoa  44154  minregex  44293  minregex2  44294  rclexi  44374  rtrclex  44376  trclubgNEW  44377  rtrclexi  44380  cnvrcl0  44384  cnvtrcl0  44385  dfrtrcl5  44388  trcleq2lemRP  44389  trficl  44428  dfrcl2  44433  relexpss1d  44464  trclrelexplem  44470  brtrclfv2  44486  dfrtrcl3  44492  heeq12  44535  ntrk2imkb  44796  clsk3nimkb  44799  clsk1independent  44805  isotone1  44807  isotone2  44808  ntrclsss  44822  ntrclsiso  44826  ntrclsk2  44827  ntrclsk3  44829  ismnu  45004  ismnushort  45044  nzss  45060  iunincfi  45845  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  meaiuninclem  47227  meaiunincf  47230  meaiuninc3v  47231  meaiuninc3  47232  meaiininclem  47233  meaiininc  47234  caragenss  47251  carageniuncllem1  47268  hoidmvle  47347  ovnhoilem2  47349  hoiqssbl  47372  ovolval5lem2  47400  vonioolem2  47428  vonicclem2  47431  isisubgr  48660  uspgrsprf  48944  scmsuppss  49184  setc1onsubc  50413