Theorem sseq2 3252

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

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

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12  3253  sseq2i  3255  sseq2d  3258  sseqtrid  3278  nssne1  3286  sseq0  3538  un00  3543  pweq  3659  ssintab  3950  ssintub  3951  intmin  3953  treq  4198  ssexg  4233  exmidundif  4302  frforeq3  4450  frirrg  4453  iunpw  4583  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  ordtri2or2exmid  4675  ontri2orexmidim  4676  iotaexab  5312  fununi  5405  funcnvuni  5406  feq3  5474  ssimaexg  5717  nnawordex  6740  ereq1  6752  xpider  6818  domeng  6966  ssfiexmid  7106  ssfiexmidt  7108  fisseneq  7170  sbthlemi4  7202  sbthlemi5  7203  nninfninc  7365  acfun  7465  onntri45  7502  ccfunen  7526  fprodssdc  12212  lspf  14465  lspval  14466  basis2  14839  eltg2  14844  clsval  14902  ntrcls0  14922  isnei  14935  neiint  14936  neipsm  14945  opnneissb  14946  opnssneib  14947  innei  14954  icnpimaex  15002  cnptoprest2  15031  neitx  15059  txcnp  15062  blssps  15218  blss  15219  metss  15285  metrest  15297  metcnp3  15302  upgredgpr  16070  wlkvtxiedg  16266  wlkvtxiedgg  16267  wlkres  16300  bdssexg  16600  bj-nntrans  16647  bj-omtrans  16652