Theorem sseq2 3126

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

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

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  sseq12  3127  sseq2i  3129  sseq2d  3132  sseqtrid  3152  nssne1  3160  sseq0  3409  un00  3414  pweq  3518  ssintab  3796  ssintub  3797  intmin  3799  treq  4040  ssexg  4075  exmidundif  4137  frforeq3  4277  frirrg  4280  iunpw  4409  ordtri2orexmid  4446  ontr2exmid  4448  onsucsssucexmid  4450  ordtri2or2exmid  4494  fununi  5199  funcnvuni  5200  feq3  5265  ssimaexg  5491  nnawordex  6432  ereq1  6444  xpider  6508  domeng  6654  ssfiexmid  6778  fisseneq  6828  sbthlemi4  6856  sbthlemi5  6857  acfun  7080  ccfunen  7096  basis2  12254  eltg2  12261  clsval  12319  ntrcls0  12339  isnei  12352  neiint  12353  neipsm  12362  opnneissb  12363  opnssneib  12364  innei  12371  icnpimaex  12419  cnptoprest2  12448  neitx  12476  txcnp  12479  blssps  12635  blss  12636  metss  12702  metrest  12714  metcnp3  12719  bdssexg  13273  bj-nntrans  13320  bj-omtrans  13325