Theorem sseq12i 3825

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 3822	. 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
4	1, 2, 3	mp2an 684	1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷)

Syntax hints:   ↔ wb 198   = wceq 1653   ⊆ wss 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781

This theorem is referenced by:  3sstr3i  3837  3sstr4i  3838  3sstr3g  3839  3sstr4g  3840  ss2rab  3872  rabsssn  4404  issubgr  26497  pjordi  29549  mdsldmd1i  29707  iuninc  29888  cvmlift2lem12  31805  brtrclfv2  38790  nzss  39286  hoidmvle  41548  ovolval5lem3  41602  fldhmsubc  42871  fldhmsubcALTV  42889