Theorem 3sstr4g 4025

Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
3sstr4g.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3sstr4g.2	⊢ 𝐶 = 𝐴
3sstr4g.3	⊢ 𝐷 = 𝐵

Assertion

Ref	Expression
3sstr4g	⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Proof of Theorem 3sstr4g

Step	Hyp	Ref	Expression
1		3sstr4g.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		3sstr4g.2	. . 3 ⊢ 𝐶 = 𝐴
3		3sstr4g.3	. . 3 ⊢ 𝐷 = 𝐵
4	2, 3	sseq12i 4010	. 2 ⊢ (𝐶 ⊆ 𝐷 ↔ 𝐴 ⊆ 𝐵)
5	1, 4	sylibr 233	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1534   ⊆ wss 3947

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-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954  df-ss 3964

This theorem is referenced by:  rabss2  4073  unss2  4181  sslin  4235  intss  4972  ssopab2  5548  xpss12  5693  coss1  5858  coss2  5859  cnvss  5875  rnss  5941  ssres  6012  ssres2  6013  imass1  6105  imass2  6106  predpredss  6312  predrelss  6343  ssoprab2  7488  ressuppss  8187  tposss  8232  onovuni  8362  ss2ixp  8928  fodomfi  9349  coss12d  14951  isumsplit  15818  isumrpcl  15821  cvgrat  15861  gsumzf1o  19866  gsumzmhm  19891  gsumzinv  19899  fldc  20671  dsmmsubg  21676  qustgpopn  24023  metnrmlem2  24775  ovolsslem  25412  uniioombllem3  25513  ulmres  26323  xrlimcnp  26899  pntlemq  27533  cusgredg  29236  sspba  30536  shlej2i  31188  chpssati  32172  iunrnmptss  32355  mptssALT  32460  pmtrcnelor  32814  rspectopn  33468  zarmxt1  33481  bnj1408  34667  subfacp1lem6  34795  mthmpps  35192  bj-gabss  36413  qsss1  37761  cossss  37897  disjdmqscossss  38275  aomclem4  42481  cotrclrcl  43172  ovnsslelem  45948  uspgrimprop  47171  fldcALTV  47394

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »