Theorem sseq12d 3946

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sscon34b  4252  ssdifeq0  4445  relcnvtrgOLD  6287  sbcfung  6583  knatar  7390  suppfnss  8234  funsssuppss  8235  csbfrecsg  8330  smogt  8403  oawordri  8586  omwordi  8607  omwordri  8608  oewordi  8628  oewordri  8629  oeworde  8630  nnawordi  8658  nnmwordi  8672  nnmwordri  8673  naddssim  8723  naddss2  8728  sbthlem2  9135  sbth  9144  sbthfi  9242  marypha2lem3  9456  hartogslem1  9563  inf3lem1  9656  dfttrcl2  9752  tcrank  9928  scottabf  9966  alephle  10194  cfsmolem  10375  isfin3ds  10434  fin23lem17  10443  fin23lem39  10455  isf32lem1  10458  isf32lem2  10459  isf32lem11  10468  isf33lem  10471  isf34lem7  10484  isf34lem6  10485  fin1a2lem13  10517  itunitc1  10525  dominf  10550  dcomex  10552  axdc2lem  10553  dominfac  10685  fpwwe2cbv  10742  fpwwe2lem2  10744  fpwwe2lem4  10746  fpwwecbv  10756  fpwwelem  10757  canthwelem  10762  canthwe  10763  pwfseqlem4  10774  wunex2  10850  swrdval  14819  trcleq2lem  15173  dfrtrcl2  15244  vdwpc  17187  vdwlem1  17188  vdwlem6  17193  vdwlem7  17194  vdwlem8  17195  isstruct2  17356  ressval  17440  mreexexlemd  17847  isacs1i  17860  isssc  18024  ssc2  18026  fullfunc  18112  fthfunc  18113  isps  18771  istsr  18786  isdir  18801  gsumvalx  18894  efgi2  19969  dmdprd  20244  dprdss  20275  dmdprdpr  20295  mhpfval  22489  scmatdmat  22860  basis1  23298  baspartn  23302  eltg  23305  cncls  23622  ispnrm  23687  1stcfb  23793  2ndcctbss  23804  1stcelcls  23810  subislly  23830  kgenidm  23896  ptpjpre1  23920  txcmplem2  23991  flimval  24312  flimcf  24331  fclscf  24374  metss  24857  isngp  24945  iscph  25521  cphsscph  25602  equivcau  25651  caubl  25659  caublcls  25660  ovoliunlem3  25855  volsuplem  25906  volsup  25907  dyaddisj  25947  itg1climres  26065  addbdaylem  28433  addbday  28434  negbdaylem  28472  addonbday  28695  bdaypw2n0bndlem  28879  bdaypw2n0bnd  28880  isausgr  29775  issubgr  29882  subgrprop3  29887  cusgrfilem1  30066  wkslem1  30218  wkslem2  30219  iswlk  30221  wlkres  30279  redwlk  30281  wlkp1lem8  30289  wlkdlem2  30292  pfxwlk  30296  crctcshwlkn0lem4  30432  crctcshwlkn0lem5  30433  crctcshwlkn0lem6  30434  2wlkdlem10  30554  3wlkdlem10  30800  eupthseg  30837  issh  31840  isch  31854  hsupss  31973  shslej  32012  shlub  32046  ledi  32172  pjoi0  32349  mdbr4  32930  dmdbr4  32938  dmdi4  32939  dmdbr5  32940  mdslle1i  32949  mdslle2i  32950  mdslmd1lem1  32957  mdslmd1lem2  32958  mdslmd1lem3  32959  mdslmd1lem4  32960  mdslmd1i  32961  sumdmdlem2  33051  resvval  33960  zhmnrg  34667  ispisys  34855  cvmliftlem3  36219  ismfs  36481  nmuladdss  37140  rdgssun  38493  poimirlem32  38762  volsupnfl  38775  elrefrels2  39722  refreleq  39725  elcnvrefrels2  39738  dfsymrels2  39749  dfsymrel2  39757  elsymrels2  39761  symreleq  39766  elrefsymrels2  39777  dftrrels2  39783  dftrrel2  39785  eltrrels2  39787  trreleq  39790  eleqvrels2  39800  lssatle  40264  pmaple  41010  2polcon4bN  41167  ispautN  41348  diaord  42296  dibord  42408  dihord6apre  42505  dihord3  42506  dihord4  42507  dihcnvord  42523  dvh4dimlem  42692  islpolN  42732  mapdordlem2  42886  mapdcnvordN  42907  mapdindp  42920  hdmaplkr  43162  ismrcd1  43902  ismrcd2  43903  ismrc  43905  incssnn0  43915  diophrw  43963  hbtlem5  44322  hbt  44324  naddgeoa  44588  minregex  44727  minregex2  44728  rclexi  44807  rtrclex  44809  trclubgNEW  44810  rtrclexi  44813  cnvrcl0  44817  cnvtrcl0  44818  dfrtrcl5  44821  trcleq2lemRP  44822  trficl  44861  dfrcl2  44866  relexpss1d  44897  trclrelexplem  44903  brtrclfv2  44919  dfrtrcl3  44925  heeq12  44968  ntrk2imkb  45229  clsk3nimkb  45232  clsk1independent  45238  isotone1  45240  isotone2  45241  ntrclsss  45255  ntrclsiso  45259  ntrclsk2  45260  ntrclsk3  45262  ismnu  45437  ismnushort  45477  nzss  45493  iunincfi  46314  fourierdlem89  47410  fourierdlem90  47411  fourierdlem91  47412  meaiuninclem  47695  meaiunincf  47698  meaiuninc3v  47699  meaiuninc3  47700  meaiininclem  47701  meaiininc  47702  caragenss  47719  carageniuncllem1  47736  hoidmvle  47815  ovnhoilem2  47817  hoiqssbl  47840  ovolval5lem2  47868  vonioolem2  47896  vonicclem2  47899  isisubgr  49165  uspgrsprf  49449  scmsuppss  49688  setc1onsubc  50945