Theorem sseq2 3204

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sseq12  3205  sseq2i  3207  sseq2d  3210  sseqtrid  3230  nssne1  3238  sseq0  3489  un00  3494  pweq  3605  ssintab  3888  ssintub  3889  intmin  3891  treq  4134  ssexg  4169  exmidundif  4236  frforeq3  4379  frirrg  4382  iunpw  4512  ordtri2orexmid  4556  ontr2exmid  4558  onsucsssucexmid  4560  ordtri2or2exmid  4604  ontri2orexmidim  4605  iotaexab  5234  fununi  5323  funcnvuni  5324  feq3  5389  ssimaexg  5620  nnawordex  6584  ereq1  6596  xpider  6662  domeng  6808  ssfiexmid  6934  fisseneq  6990  sbthlemi4  7021  sbthlemi5  7022  nninfninc  7184  acfun  7269  onntri45  7303  ccfunen  7326  fprodssdc  11736  lspf  13888  lspval  13889  basis2  14227  eltg2  14232  clsval  14290  ntrcls0  14310  isnei  14323  neiint  14324  neipsm  14333  opnneissb  14334  opnssneib  14335  innei  14342  icnpimaex  14390  cnptoprest2  14419  neitx  14447  txcnp  14450  blssps  14606  blss  14607  metss  14673  metrest  14685  metcnp3  14690  bdssexg  15466  bj-nntrans  15513  bj-omtrans  15518