Theorem sseq12i 3977

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

Syntax hints:   ↔ wb 205   = wceq 1541   ⊆ wss 3913

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  3sstr3i  3989  3sstr4i  3990  3sstr3g  3991  3sstr4g  3992  ss2rab  4033  rabsssn  4633  issubgr  28282  pjordi  31178  mdsldmd1i  31336  iuninc  31546  cvmlift2lem12  33995  brtrclfv2  42121  nzss  42719  hoidmvle  44961  fldhmsubc  46502  fldhmsubcALTV  46520