Theorem sseq12d 3257

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

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

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 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  3sstr3d  3270  3sstr4d  3271  ssdifeq0  3576  relcnvtr  5258  rdgisucinc  6556  oawordriexmid  6643  nnaword  6684  nnawordi  6688  sbthlem2  7162  isbth  7171  nninff  7326  nninfninc  7327  infnninf  7328  infnninfOLD  7329  nnnninf  7330  nnnninfeq  7332  nnnninfeq2  7333  nninfwlpoimlemg  7379  swrdval  11238  ennnfonelemkh  13056  ennnfonelemrnh  13060  isstruct2im  13115  isstruct2r  13116  basis1  14800  baspartn  14803  eltg  14805  metss  15247  isausgren  16047  issubgr  16137  subgrprop3  16142  wkslem1  16200  wkslem2  16201  iswlk  16203  wlkres  16259  eupthseg  16332  0nninf  16669  nnsf  16670  peano4nninf  16671  nninfalllem1  16673  nninfself  16678