Theorem sseq2 3251

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

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

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sseq12  3252  sseq2i  3254  sseq2d  3257  sseqtrid  3277  nssne1  3285  sseq0  3536  un00  3541  pweq  3655  ssintab  3945  ssintub  3946  intmin  3948  treq  4193  ssexg  4228  exmidundif  4296  frforeq3  4444  frirrg  4447  iunpw  4577  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  ordtri2or2exmid  4669  ontri2orexmidim  4670  iotaexab  5305  fununi  5398  funcnvuni  5399  feq3  5467  ssimaexg  5708  nnawordex  6697  ereq1  6709  xpider  6775  domeng  6923  ssfiexmid  7063  ssfiexmidt  7065  fisseneq  7127  sbthlemi4  7159  sbthlemi5  7160  nninfninc  7322  acfun  7422  onntri45  7459  ccfunen  7483  fprodssdc  12156  lspf  14409  lspval  14410  basis2  14778  eltg2  14783  clsval  14841  ntrcls0  14861  isnei  14874  neiint  14875  neipsm  14884  opnneissb  14885  opnssneib  14886  innei  14893  icnpimaex  14941  cnptoprest2  14970  neitx  14998  txcnp  15001  blssps  15157  blss  15158  metss  15224  metrest  15236  metcnp3  15241  upgredgpr  16006  wlkvtxiedg  16202  wlkvtxiedgg  16203  wlkres  16236  bdssexg  16525  bj-nntrans  16572  bj-omtrans  16577