NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  sikexlem Unicode version

Theorem sikexlem 4295
Description: Lemma for sikexg 4296. Equality for two subsets of 1c squared . (Contributed by SF, 14-Jan-2015.)
Hypotheses
Ref Expression
sikexlem.1 1c k 1c
sikexlem.2 1c k 1c
Assertion
Ref Expression
sikexlem
Distinct variable groups:   ,,   ,,

Proof of Theorem sikexlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sikexlem.1 . . 3 1c k 1c
2 sikexlem.2 . . 3 1c k 1c
3 ssofeq 4077 . . 3 1c k 1c 1c k 1c 1c k 1c
41, 2, 3mp2an 653 . 2 1c k 1c
5 df-ral 2619 . . 3 1c k 1c 1c k 1c
6 elxpk 4196 . . . . . . . 8 1c k 1c 1c 1c
7 el1c 4139 . . . . . . . . . . . . . 14 1c
8 el1c 4139 . . . . . . . . . . . . . 14 1c
97, 8anbi12i 678 . . . . . . . . . . . . 13 1c 1c
10 eeanv 1913 . . . . . . . . . . . . 13
119, 10bitr4i 243 . . . . . . . . . . . 12 1c 1c
1211anbi2i 675 . . . . . . . . . . 11 1c 1c
13 df-3an 936 . . . . . . . . . . . . . 14
14 ancom 437 . . . . . . . . . . . . . 14
1513, 14bitri 240 . . . . . . . . . . . . 13
16152exbii 1583 . . . . . . . . . . . 12
17 19.42vv 1907 . . . . . . . . . . . 12
1816, 17bitri 240 . . . . . . . . . . 11
1912, 18bitr4i 243 . . . . . . . . . 10 1c 1c
20192exbii 1583 . . . . . . . . 9 1c 1c
21 exrot4 1745 . . . . . . . . 9
2220, 21bitr4i 243 . . . . . . . 8 1c 1c
23 snex 4111 . . . . . . . . . 10
24 snex 4111 . . . . . . . . . 10
25 opkeq1 4059 . . . . . . . . . . 11
2625eqeq2d 2364 . . . . . . . . . 10
27 opkeq2 4060 . . . . . . . . . . 11
2827eqeq2d 2364 . . . . . . . . . 10
2923, 24, 26, 28ceqsex2v 2896 . . . . . . . . 9
30292exbii 1583 . . . . . . . 8
316, 22, 303bitri 262 . . . . . . 7 1c k 1c
3231imbi1i 315 . . . . . 6 1c k 1c
33 19.23vv 1892 . . . . . 6
3432, 33bitr4i 243 . . . . 5 1c k 1c
3534albii 1566 . . . 4 1c k 1c
36 alrot3 1738 . . . 4
3735, 36bitri 240 . . 3 1c k 1c
38 opkex 4113 . . . . 5
39 eleq1 2413 . . . . . 6
40 eleq1 2413 . . . . . 6
4139, 40bibi12d 312 . . . . 5
4238, 41ceqsalv 2885 . . . 4
43422albii 1567 . . 3
445, 37, 433bitri 262 . 2 1c k 1c
454, 44bitri 240 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wal 1540  wex 1541   wceq 1642   wcel 1710  wral 2614   wss 3257  csn 3737  copk 4057  1cc1c 4134   k cxpk 4174
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741  df-pr 3742  df-opk 4058  df-1c 4136  df-xpk 4185
This theorem is referenced by:  sikexg  4296
  Copyright terms: Public domain W3C validator