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  12301  lspf  14649  lspval  14650  basis2  15025  eltg2  15030  clsval  15088  ntrcls0  15108  isnei  15121  neiint  15122  neipsm  15131  opnneissb  15132  opnssneib  15133  innei  15140  icnpimaex  15188  cnptoprest2  15217  neitx  15245  txcnp  15248  blssps  15404  blss  15405  metss  15471  metrest  15483  metcnp3  15488  upgredgpr  16256  wlkvtxiedg  16452  wlkvtxiedgg  16453  wlkres  16486  bdssexg  16786  bj-nntrans  16833  bj-omtrans  16838