Theorem sseq12d 3258

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
sseq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
sseq12d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	sseq1d 3256	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3257	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397   ⊆ wss 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  3sstr3d  3271  3sstr4d  3272  ssdifeq0  3577  relcnvtr  5256  rdgisucinc  6551  oawordriexmid  6638  nnaword  6679  nnawordi  6683  sbthlem2  7157  isbth  7166  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfwlpoimlemg  7374  swrdval  11230  ennnfonelemkh  13035  ennnfonelemrnh  13039  isstruct2im  13094  isstruct2r  13095  basis1  14774  baspartn  14777  eltg  14779  metss  15221  isausgren  16021  issubgr  16111  subgrprop3  16116  wkslem1  16174  wkslem2  16175  iswlk  16177  wlkres  16233  eupthseg  16306  0nninf  16627  nnsf  16628  peano4nninf  16629  nninfalllem1  16631  nninfself  16636