Theorem sseq2 3272

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

Ref	Expression
sseq2	⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3255	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 30	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3255	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 30	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 338	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3263	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 392	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 201	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12  3273  sseq2i  3275  sseq2d  3278  sseqtrid  3298  nssne1  3306  sseq0b  3564  un00  3567  pweq  3691  ssintab  3985  ssintub  3986  intmin  3988  treq  4233  ssexg  4270  exmidundif  4341  frforeq3  4490  frirrg  4493  iunpw  4624  ordtri2orexmid  4668  ontr2exmid  4670  onsucsssucexmid  4672  ordtri2or2exmid  4716  ontri2orexmidim  4717  iotaexab  5354  fununi  5447  funcnvuni  5448  feq3  5516  ssimaexg  5762  nnawordex  6796  ereq1  6808  xpider  6874  domeng  7030  ssfiexmid  7172  ssfiexmidt  7174  fisseneq  7236  sbthlemi4  7271  sbthlemi5  7272  nninfninc  7457  acfun  7557  onntri45  7594  ccfunen  7624  fprodssdc  12340  lspf  14709  lspval  14710  aspval  14998  asplss  14999  aspsubrg  15001  basis2  15132  eltg2  15137  clsval  15195  ntrcls0  15215  isnei  15228  neiint  15229  neipsm  15238  opnneissb  15239  opnssneib  15240  innei  15247  icnpimaex  15295  cnptoprest2  15324  neitx  15352  txcnp  15355  blssps  15511  blss  15512  metss  15578  metrest  15590  metcnp3  15595  upgredgpr  16373  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlkres  16603  bdssexg  16913  bj-nntrans  16960  bj-omtrans  16965