Theorem sseq2 3261

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

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

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  sseq12  3262  sseq2i  3264  sseq2d  3267  sseqtrid  3287  nssne1  3295  sseq0  3549  un00  3554  pweq  3671  ssintab  3965  ssintub  3966  intmin  3968  treq  4213  ssexg  4248  exmidundif  4318  frforeq3  4467  frirrg  4470  iunpw  4600  ordtri2orexmid  4644  ontr2exmid  4646  onsucsssucexmid  4648  ordtri2or2exmid  4692  ontri2orexmidim  4693  iotaexab  5330  fununi  5423  funcnvuni  5424  feq3  5492  ssimaexg  5738  nnawordex  6761  ereq1  6773  xpider  6839  domeng  6988  ssfiexmid  7130  ssfiexmidt  7132  fisseneq  7194  sbthlemi4  7229  sbthlemi5  7230  nninfninc  7413  acfun  7513  onntri45  7550  ccfunen  7577  fprodssdc  12272  lspf  14529  lspval  14530  basis2  14905  eltg2  14910  clsval  14968  ntrcls0  14988  isnei  15001  neiint  15002  neipsm  15011  opnneissb  15012  opnssneib  15013  innei  15020  icnpimaex  15068  cnptoprest2  15097  neitx  15125  txcnp  15128  blssps  15284  blss  15285  metss  15351  metrest  15363  metcnp3  15368  upgredgpr  16136  wlkvtxiedg  16332  wlkvtxiedgg  16333  wlkres  16366  bdssexg  16666  bj-nntrans  16713  bj-omtrans  16718