Theorem sseq12d 3235

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 3233	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3234	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1375   ⊆ wss 3177

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190

This theorem is referenced by:  3sstr3d  3248  3sstr4d  3249  ssdifeq0  3554  relcnvtr  5224  rdgisucinc  6501  oawordriexmid  6586  nnaword  6627  nnawordi  6631  sbthlem2  7093  isbth  7102  nninff  7257  nninfninc  7258  infnninf  7259  infnninfOLD  7260  nnnninf  7261  nnnninfeq  7263  nnnninfeq2  7264  nninfwlpoimlemg  7310  swrdval  11146  ennnfonelemkh  12949  ennnfonelemrnh  12953  isstruct2im  13008  isstruct2r  13009  basis1  14686  baspartn  14689  eltg  14691  metss  15133  isausgren  15930  0nninf  16281  nnsf  16282  peano4nninf  16283  nninfalllem1  16285  nninfself  16290