Theorem sseq2 3248

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

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

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 3203  df-ss 3210

This theorem is referenced by:  sseq12  3249  sseq2i  3251  sseq2d  3254  sseqtrid  3274  nssne1  3282  sseq0  3533  un00  3538  pweq  3652  ssintab  3940  ssintub  3941  intmin  3943  treq  4188  ssexg  4223  exmidundif  4291  frforeq3  4439  frirrg  4442  iunpw  4572  ordtri2orexmid  4616  ontr2exmid  4618  onsucsssucexmid  4620  ordtri2or2exmid  4664  ontri2orexmidim  4665  iotaexab  5300  fununi  5392  funcnvuni  5393  feq3  5461  ssimaexg  5701  nnawordex  6688  ereq1  6700  xpider  6766  domeng  6914  ssfiexmid  7051  fisseneq  7112  sbthlemi4  7143  sbthlemi5  7144  nninfninc  7306  acfun  7405  onntri45  7442  ccfunen  7466  fprodssdc  12122  lspf  14374  lspval  14375  basis2  14743  eltg2  14748  clsval  14806  ntrcls0  14826  isnei  14839  neiint  14840  neipsm  14849  opnneissb  14850  opnssneib  14851  innei  14858  icnpimaex  14906  cnptoprest2  14935  neitx  14963  txcnp  14966  blssps  15122  blss  15123  metss  15189  metrest  15201  metcnp3  15206  upgredgpr  15968  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlkres  16149  bdssexg  16376  bj-nntrans  16423  bj-omtrans  16428