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

Theorem insklem 4304
 Description: Lemma for ins2kexg 4305 and ins3kexg 4306. Equality for subsets of 1 1c k k . (Contributed by SF, 14-Jan-2015.)
Hypotheses
Ref Expression
insklem.1 1 1c k k
insklem.2 1 1c k k
Assertion
Ref Expression
insklem
Distinct variable groups:   ,,,   ,,,

Proof of Theorem insklem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 insklem.1 . . 3 1 1c k k
2 insklem.2 . . 3 1 1c k k
3 ssofeq 4077 . . 3 1 1c k k 1 1c k k 1 1c k k
41, 2, 3mp2an 653 . 2 1 1c k k
5 19.23v 1891 . . . . 5
6 19.23vv 1892 . . . . . 6
76albii 1566 . . . . 5
8 19.42vv 1907 . . . . . . . . . 10 1 1c 1 1c
98anbi2i 675 . . . . . . . . 9 1 1c 1 1c
10 19.42vv 1907 . . . . . . . . 9 1 1c 1 1c
11 elvvk 4207 . . . . . . . . . . 11 k
1211anbi2i 675 . . . . . . . . . 10 1 1c k 1 1c
1312anbi2i 675 . . . . . . . . 9 1 1c k 1 1c
149, 10, 133bitr4ri 269 . . . . . . . 8 1 1c k 1 1c
15142exbii 1583 . . . . . . 7 1 1c k 1 1c
16 elxpk 4196 . . . . . . 7 1 1c k k 1 1c k
17 exrot3 1744 . . . . . . . 8
18 exancom 1586 . . . . . . . . . . . 12 1 1c 1 1c
19 elpw11c 4147 . . . . . . . . . . . . . . 15 1 1c
2019anbi1i 676 . . . . . . . . . . . . . 14 1 1c
21 19.41v 1901 . . . . . . . . . . . . . 14
2220, 21bitr4i 243 . . . . . . . . . . . . 13 1 1c
2322exbii 1582 . . . . . . . . . . . 12 1 1c
2418, 23bitri 240 . . . . . . . . . . 11 1 1c
25 ancom 437 . . . . . . . . . . . . . . 15 1 1c 1 1c
2625anbi2i 675 . . . . . . . . . . . . . 14 1 1c 1 1c
27 an12 772 . . . . . . . . . . . . . 14 1 1c 1 1c
2826, 27bitri 240 . . . . . . . . . . . . 13 1 1c 1 1c
29282exbii 1583 . . . . . . . . . . . 12 1 1c 1 1c
30 opkex 4113 . . . . . . . . . . . . . 14
31 opkeq2 4060 . . . . . . . . . . . . . . . 16
3231eqeq2d 2364 . . . . . . . . . . . . . . 15
3332anbi1d 685 . . . . . . . . . . . . . 14 1 1c 1 1c
3430, 33ceqsexv 2894 . . . . . . . . . . . . 13 1 1c 1 1c
3534exbii 1582 . . . . . . . . . . . 12 1 1c 1 1c
3629, 35bitri 240 . . . . . . . . . . 11 1 1c 1 1c
37 snex 4111 . . . . . . . . . . . . . 14
38 opkeq1 4059 . . . . . . . . . . . . . . 15
3938eqeq2d 2364 . . . . . . . . . . . . . 14
4037, 39ceqsexv 2894 . . . . . . . . . . . . 13
4140exbii 1582 . . . . . . . . . . . 12
42 excom 1741 . . . . . . . . . . . 12
4341, 42bitr3i 242 . . . . . . . . . . 11
4424, 36, 433bitr4ri 269 . . . . . . . . . 10 1 1c
45442exbii 1583 . . . . . . . . 9 1 1c
46 exrot4 1745 . . . . . . . . 9 1 1c 1 1c
4745, 46bitri 240 . . . . . . . 8 1 1c
4817, 47bitri 240 . . . . . . 7 1 1c
4915, 16, 483bitr4i 268 . . . . . 6 1 1c k k
5049imbi1i 315 . . . . 5 1 1c k k
515, 7, 503bitr4ri 269 . . . 4 1 1c k k
5251albii 1566 . . 3 1 1c k k
53 df-ral 2619 . . 3 1 1c k k 1 1c k k
54 alcom 1737 . . . 4
55 alrot3 1738 . . . . 5
5655albii 1566 . . . 4
57 opkex 4113 . . . . . . 7
58 eleq1 2413 . . . . . . . 8
59 eleq1 2413 . . . . . . . 8
6058, 59bibi12d 312 . . . . . . 7
6157, 60ceqsalv 2885 . . . . . 6
6261albii 1566 . . . . 5
63622albii 1567 . . . 4
6454, 56, 633bitrri 263 . . 3
6552, 53, 643bitr4i 268 . 2 1 1c k k
664, 65bitri 240 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 176   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  wral 2614  cvv 2859   wss 3257  csn 3737  copk 4057  1cc1c 4134  1 cpw1 4135   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-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-rex 2620  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-pw 3724  df-sn 3741  df-pr 3742  df-opk 4058  df-1c 4136  df-pw1 4137  df-xpk 4185 This theorem is referenced by:  ins2kexg  4305  ins3kexg  4306
 Copyright terms: Public domain W3C validator