Theorem sseq2 3249

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sseq12  3250  sseq2i  3252  sseq2d  3255  sseqtrid  3275  nssne1  3283  sseq0  3534  un00  3539  pweq  3653  ssintab  3943  ssintub  3944  intmin  3946  treq  4191  ssexg  4226  exmidundif  4294  frforeq3  4442  frirrg  4445  iunpw  4575  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  ordtri2or2exmid  4667  ontri2orexmidim  4668  iotaexab  5303  fununi  5395  funcnvuni  5396  feq3  5464  ssimaexg  5704  nnawordex  6692  ereq1  6704  xpider  6770  domeng  6918  ssfiexmid  7058  ssfiexmidt  7060  fisseneq  7121  sbthlemi4  7153  sbthlemi5  7154  nninfninc  7316  acfun  7415  onntri45  7452  ccfunen  7476  fprodssdc  12144  lspf  14396  lspval  14397  basis2  14765  eltg2  14770  clsval  14828  ntrcls0  14848  isnei  14861  neiint  14862  neipsm  14871  opnneissb  14872  opnssneib  14873  innei  14880  icnpimaex  14928  cnptoprest2  14957  neitx  14985  txcnp  14988  blssps  15144  blss  15145  metss  15211  metrest  15223  metcnp3  15228  upgredgpr  15993  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlkres  16188  bdssexg  16449  bj-nntrans  16496  bj-omtrans  16501