Theorem sseq12i 3964

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

Syntax hints:   ↔ wb 208   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  ss2rab  4020  rabsssn  4624  fldhmsubc  20822  issubgr  29429  pjordi  32333  mdsldmd1i  32491  rabsspr  32660  rabsstp  32661  iuninc  32720  cvmlift2lem12  35625  brtrclfv2  44264  nzss  44854  hoidmvle  47135  fldhmsubcALTV  48916