Theorem sseq2 3221

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 3204	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 30	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3204	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 30	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 338	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3212	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 388	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 201	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  sseq12  3222  sseq2i  3224  sseq2d  3227  sseqtrid  3247  nssne1  3255  sseq0  3506  un00  3511  pweq  3623  ssintab  3907  ssintub  3908  intmin  3910  treq  4155  ssexg  4190  exmidundif  4257  frforeq3  4401  frirrg  4404  iunpw  4534  ordtri2orexmid  4578  ontr2exmid  4580  onsucsssucexmid  4582  ordtri2or2exmid  4626  ontri2orexmidim  4627  iotaexab  5258  fununi  5350  funcnvuni  5351  feq3  5419  ssimaexg  5653  nnawordex  6627  ereq1  6639  xpider  6705  domeng  6853  ssfiexmid  6987  fisseneq  7045  sbthlemi4  7076  sbthlemi5  7077  nninfninc  7239  acfun  7334  onntri45  7368  ccfunen  7391  fprodssdc  11971  lspf  14221  lspval  14222  basis2  14590  eltg2  14595  clsval  14653  ntrcls0  14673  isnei  14686  neiint  14687  neipsm  14696  opnneissb  14697  opnssneib  14698  innei  14705  icnpimaex  14753  cnptoprest2  14782  neitx  14810  txcnp  14813  blssps  14969  blss  14970  metss  15036  metrest  15048  metcnp3  15053  bdssexg  15974  bj-nntrans  16021  bj-omtrans  16026