Theorem sseq2 3121

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 3104	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 30	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3104	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 30	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 336	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3112	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 385	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 200	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ⊆ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  sseq12  3122  sseq2i  3124  sseq2d  3127  sseqtrid  3147  nssne1  3155  sseq0  3404  un00  3409  pweq  3513  ssintab  3788  ssintub  3789  intmin  3791  treq  4032  ssexg  4067  exmidundif  4129  frforeq3  4269  frirrg  4272  iunpw  4401  ordtri2orexmid  4438  ontr2exmid  4440  onsucsssucexmid  4442  ordtri2or2exmid  4486  fununi  5191  funcnvuni  5192  feq3  5257  ssimaexg  5483  nnawordex  6424  ereq1  6436  xpider  6500  domeng  6646  ssfiexmid  6770  fisseneq  6820  sbthlemi4  6848  sbthlemi5  6849  acfun  7063  ccfunen  7079  basis2  12215  eltg2  12222  clsval  12280  ntrcls0  12300  isnei  12313  neiint  12314  neipsm  12323  opnneissb  12324  opnssneib  12325  innei  12332  icnpimaex  12380  cnptoprest2  12409  neitx  12437  txcnp  12440  blssps  12596  blss  12597  metss  12663  metrest  12675  metcnp3  12680  bdssexg  13102  bj-nntrans  13149  bj-omtrans  13154