Theorem sseq12i 3951

Description: An equality inference for the subclass relationship. (Contributed by NM, 31-May-1999.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)

Hypotheses

Ref	Expression
sseq1i.1	⊢ 𝐴 = 𝐵
sseq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
sseq12i	⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)

Proof of Theorem sseq12i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sseq12i.2	. 2 ⊢ 𝐶 = 𝐷
3		sseq12 3948	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
4	1, 2, 3	mp2an 689	1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)

Syntax hints:   ↔ wb 205   = wceq 1539   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  3sstr3i  3963  3sstr4i  3964  3sstr3g  3965  3sstr4g  3966  ss2rab  4004  rabsssn  4603  issubgr  27638  pjordi  30535  mdsldmd1i  30693  iuninc  30900  cvmlift2lem12  33276  brtrclfv2  41335  nzss  41935  hoidmvle  44138  ovolval5lem3  44192  fldhmsubc  45642  fldhmsubcALTV  45660