Theorem sseq2 3180

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  sseq12  3181  sseq2i  3183  sseq2d  3186  sseqtrid  3206  nssne1  3214  sseq0  3465  un00  3470  pweq  3579  ssintab  3862  ssintub  3863  intmin  3865  treq  4108  ssexg  4143  exmidundif  4207  frforeq3  4348  frirrg  4351  iunpw  4481  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  ordtri2or2exmid  4571  ontri2orexmidim  4572  fununi  5285  funcnvuni  5286  feq3  5351  ssimaexg  5579  nnawordex  6530  ereq1  6542  xpider  6606  domeng  6752  ssfiexmid  6876  fisseneq  6931  sbthlemi4  6959  sbthlemi5  6960  acfun  7206  onntri45  7240  ccfunen  7263  fprodssdc  11598  basis2  13551  eltg2  13556  clsval  13614  ntrcls0  13634  isnei  13647  neiint  13648  neipsm  13657  opnneissb  13658  opnssneib  13659  innei  13666  icnpimaex  13714  cnptoprest2  13743  neitx  13771  txcnp  13774  blssps  13930  blss  13931  metss  13997  metrest  14009  metcnp3  14014  bdssexg  14659  bj-nntrans  14706  bj-omtrans  14711