Theorem sseq12d 4017

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  sscon34b  4304  ssdifeq0  4487  relcnvtrg  6286  knatar  7377  suppfnss  8214  funsssuppss  8215  csbfrecsg  8309  smogt  8407  oawordri  8588  omwordi  8609  omwordri  8610  oewordi  8629  oewordri  8630  oeworde  8631  nnawordi  8659  nnmwordi  8673  nnmwordri  8674  naddssim  8723  naddss2  8728  sbthlem2  9124  sbth  9133  sbthfi  9239  marypha2lem3  9477  hartogslem1  9582  inf3lem1  9668  dfttrcl2  9764  tcrank  9924  alephle  10128  cfsmolem  10310  isfin3ds  10369  fin23lem17  10378  fin23lem39  10390  isf32lem1  10393  isf32lem2  10394  isf32lem11  10403  isf33lem  10406  isf34lem7  10419  isf34lem6  10420  fin1a2lem13  10452  itunitc1  10460  dominf  10485  dcomex  10487  axdc2lem  10488  dominfac  10613  fpwwe2cbv  10670  fpwwe2lem2  10672  fpwwe2lem4  10674  fpwwecbv  10684  fpwwelem  10685  canthwelem  10690  canthwe  10691  pwfseqlem4  10702  wunex2  10778  swrdval  14681  trcleq2lem  15030  dfrtrcl2  15101  vdwpc  17018  vdwlem1  17019  vdwlem6  17024  vdwlem7  17025  vdwlem8  17026  isstruct2  17186  ressval  17277  mreexexlemd  17687  isacs1i  17700  isssc  17864  ssc2  17866  fullfunc  17953  fthfunc  17954  isps  18613  istsr  18628  isdir  18643  gsumvalx  18689  efgi2  19743  dmdprd  20018  dprdss  20049  dmdprdpr  20069  mhpfval  22142  scmatdmat  22521  basis1  22957  baspartn  22961  eltg  22964  cncls  23282  ispnrm  23347  1stcfb  23453  2ndcctbss  23463  1stcelcls  23469  subislly  23489  kgenidm  23555  ptpjpre1  23579  txcmplem2  23650  flimval  23971  flimcf  23990  fclscf  24033  metss  24521  isngp  24609  iscph  25204  cphsscph  25285  equivcau  25334  caubl  25342  caublcls  25343  ovoliunlem3  25539  volsuplem  25590  volsup  25591  dyaddisj  25631  itg1climres  25749  addsbdaylem  28049  addsbday  28050  negsbdaylem  28088  isausgr  29181  issubgr  29288  subgrprop3  29293  cusgrfilem1  29473  wkslem1  29625  wkslem2  29626  iswlk  29628  wlkres  29688  redwlk  29690  wlkp1lem8  29698  wlkdlem2  29701  crctcshwlkn0lem4  29833  crctcshwlkn0lem5  29834  crctcshwlkn0lem6  29835  2wlkdlem10  29955  3wlkdlem10  30188  eupthseg  30225  issh  31227  isch  31241  hsupss  31360  shslej  31399  shlub  31433  ledi  31559  pjoi0  31736  mdbr4  32317  dmdbr4  32325  dmdi4  32326  dmdbr5  32327  mdslle1i  32336  mdslle2i  32337  mdslmd1lem1  32344  mdslmd1lem2  32345  mdslmd1lem3  32346  mdslmd1lem4  32347  mdslmd1i  32348  sumdmdlem2  32438  resvval  33353  zhmnrg  33966  ispisys  34153  pfxwlk  35129  cvmliftlem3  35292  ismfs  35554  rdgssun  37379  poimirlem32  37659  volsupnfl  37672  elrefrels2  38519  refreleq  38522  elcnvrefrels2  38535  dfsymrels2  38546  dfsymrel2  38550  elsymrels2  38554  symreleq  38559  elrefsymrels2  38570  dftrrels2  38576  dftrrel2  38578  eltrrels2  38580  trreleq  38583  eleqvrels2  38593  lssatle  39016  pmaple  39763  2polcon4bN  39920  ispautN  40101  diaord  41049  dibord  41161  dihord6apre  41258  dihord3  41259  dihord4  41260  dihcnvord  41276  dvh4dimlem  41445  islpolN  41485  mapdordlem2  41639  mapdcnvordN  41660  mapdindp  41673  hdmaplkr  41915  ismrcd1  42709  ismrcd2  42710  ismrc  42712  incssnn0  42722  diophrw  42770  hbtlem5  43140  hbt  43142  naddgeoa  43407  minregex  43547  minregex2  43548  rclexi  43628  rtrclex  43630  trclubgNEW  43631  rtrclexi  43634  cnvrcl0  43638  cnvtrcl0  43639  dfrtrcl5  43642  trcleq2lemRP  43643  trficl  43682  dfrcl2  43687  relexpss1d  43718  trclrelexplem  43724  brtrclfv2  43740  dfrtrcl3  43746  heeq12  43789  ntrk2imkb  44050  clsk3nimkb  44053  clsk1independent  44059  isotone1  44061  isotone2  44062  ntrclsss  44076  ntrclsiso  44080  ntrclsk2  44081  ntrclsk3  44083  scottabf  44259  ismnu  44280  ismnushort  44320  nzss  44336  iunincfi  45099  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  meaiuninclem  46495  meaiunincf  46498  meaiuninc3v  46499  meaiuninc3  46500  meaiininclem  46501  meaiininc  46502  caragenss  46519  carageniuncllem1  46536  hoidmvle  46615  ovnhoilem2  46617  hoiqssbl  46640  ovolval5lem2  46668  vonioolem2  46696  vonicclem2  46699  isisubgr  47848  uspgrsprf  48062  scmsuppss  48287