Theorem sseq2 3171

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

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

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sseq12  3172  sseq2i  3174  sseq2d  3177  sseqtrid  3197  nssne1  3205  sseq0  3455  un00  3460  pweq  3567  ssintab  3846  ssintub  3847  intmin  3849  treq  4091  ssexg  4126  exmidundif  4190  frforeq3  4330  frirrg  4333  iunpw  4463  ordtri2orexmid  4505  ontr2exmid  4507  onsucsssucexmid  4509  ordtri2or2exmid  4553  ontri2orexmidim  4554  fununi  5264  funcnvuni  5265  feq3  5330  ssimaexg  5556  nnawordex  6506  ereq1  6518  xpider  6582  domeng  6728  ssfiexmid  6852  fisseneq  6907  sbthlemi4  6935  sbthlemi5  6936  acfun  7177  onntri45  7211  ccfunen  7219  fprodssdc  11546  basis2  12805  eltg2  12812  clsval  12870  ntrcls0  12890  isnei  12903  neiint  12904  neipsm  12913  opnneissb  12914  opnssneib  12915  innei  12922  icnpimaex  12970  cnptoprest2  12999  neitx  13027  txcnp  13030  blssps  13186  blss  13187  metss  13253  metrest  13265  metcnp3  13270  bdssexg  13904  bj-nntrans  13951  bj-omtrans  13956