Theorem sseq2 3266

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  sseq12  3267  sseq2i  3269  sseq2d  3272  sseqtrid  3292  nssne1  3300  sseq0  3554  un00  3559  pweq  3677  ssintab  3971  ssintub  3972  intmin  3974  treq  4219  ssexg  4254  exmidundif  4324  frforeq3  4473  frirrg  4476  iunpw  4606  ordtri2orexmid  4650  ontr2exmid  4652  onsucsssucexmid  4654  ordtri2or2exmid  4698  ontri2orexmidim  4699  iotaexab  5336  fununi  5429  funcnvuni  5430  feq3  5498  ssimaexg  5744  nnawordex  6775  ereq1  6787  xpider  6853  domeng  7002  ssfiexmid  7144  ssfiexmidt  7146  fisseneq  7208  sbthlemi4  7243  sbthlemi5  7244  nninfninc  7427  acfun  7527  onntri45  7564  ccfunen  7594  fprodssdc  12305  lspf  14667  lspval  14668  basis2  15043  eltg2  15048  clsval  15106  ntrcls0  15126  isnei  15139  neiint  15140  neipsm  15149  opnneissb  15150  opnssneib  15151  innei  15158  icnpimaex  15206  cnptoprest2  15235  neitx  15263  txcnp  15266  blssps  15422  blss  15423  metss  15489  metrest  15501  metcnp3  15506  upgredgpr  16274  wlkvtxiedg  16470  wlkvtxiedgg  16471  wlkres  16504  bdssexg  16814  bj-nntrans  16861  bj-omtrans  16866