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

Theorem eqpw1relk 4479
Description: Represent equality to unit power class via a Kuratowski relationship. (Contributed by SF, 21-Jan-2015.)
Hypotheses
Ref Expression
eqpw1relk.1
eqpw1relk.2
Assertion
Ref Expression
eqpw1relk 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1

Proof of Theorem eqpw1relk
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snex 4111 . . . . 5
2 eqpw1relk.1 . . . . . 6
32, 1opkelxpk 4248 . . . . 5 1c k 1c
41, 3mpbiran2 885 . . . 4 1c k 1c
52elpw 3728 . . . 4 1c 1c
64, 5bitri 240 . . 3 1c k 1c
7 opkex 4113 . . . . . . 7
87elimak 4259 . . . . . 6 Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1 1 1 1c Ins3k Sk Ins2k SIk Sk
9 elpw131c 4149 . . . . . . . . . 10 1 1 1 1c
109anbi1i 676 . . . . . . . . 9 1 1 1 1c Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
11 19.41v 1901 . . . . . . . . 9 Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
1210, 11bitr4i 243 . . . . . . . 8 1 1 1 1c Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
1312exbii 1582 . . . . . . 7 1 1 1 1c Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
14 df-rex 2620 . . . . . . 7 1 1 1 1c Ins3k Sk Ins2k SIk Sk 1 1 1 1c Ins3k Sk Ins2k SIk Sk
15 excom 1741 . . . . . . 7 Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
1613, 14, 153bitr4i 268 . . . . . 6 1 1 1 1c Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
178, 16bitri 240 . . . . 5 Ins3k Sk Ins2k SIk Sk k1 1 1 1c Ins3k Sk Ins2k SIk Sk
18 snex 4111 . . . . . . . 8
19 opkeq1 4059 . . . . . . . . 9
2019eleq1d 2419 . . . . . . . 8 Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
2118, 20ceqsexv 2894 . . . . . . 7 Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
22 elsymdif 3223 . . . . . . . 8 Ins3k Sk Ins2k SIk Sk Ins3k Sk Ins2k SIk Sk
23 snex 4111 . . . . . . . . . . 11
2423, 2, 1otkelins3k 4256 . . . . . . . . . 10 Ins3k Sk Sk
25 snex 4111 . . . . . . . . . . 11
2625, 2elssetk 4270 . . . . . . . . . 10 Sk
2724, 26bitri 240 . . . . . . . . 9 Ins3k Sk
2823, 2, 1otkelins2k 4255 . . . . . . . . . 10 Ins2k SIk Sk SIk Sk
29 eqpw1relk.2 . . . . . . . . . . . 12
3025, 29opksnelsik 4265 . . . . . . . . . . 11 SIk Sk Sk
31 vex 2862 . . . . . . . . . . . 12
3231, 29elssetk 4270 . . . . . . . . . . 11 Sk
3330, 32bitri 240 . . . . . . . . . 10 SIk Sk
3428, 33bitri 240 . . . . . . . . 9 Ins2k SIk Sk
3527, 34bibi12i 306 . . . . . . . 8 Ins3k Sk Ins2k SIk Sk
3622, 35xchbinx 301 . . . . . . 7 Ins3k Sk Ins2k SIk Sk
3721, 36bitri 240 . . . . . 6 Ins3k Sk Ins2k SIk Sk
3837exbii 1582 . . . . 5 Ins3k Sk Ins2k SIk Sk
39 exnal 1574 . . . . 5
4017, 38, 393bitrri 263 . . . 4 Ins3k Sk Ins2k SIk Sk k1 1 1 1c
4140con1bii 321 . . 3 Ins3k Sk Ins2k SIk Sk k1 1 1 1c
426, 41anbi12i 678 . 2 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1c
43 eldif 3221 . 2 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c
44 eqpw1 4162 . 2 1 1c
4542, 43, 443bitr4i 268 1 1c k Ins3k Sk Ins2k SIk Sk k1 1 1 1c 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wb 176   wa 358  wal 1540  wex 1541   wceq 1642   wcel 1710  wrex 2615  cvv 2859   cdif 3206   csymdif 3209   wss 3257  cpw 3722  csn 3737  copk 4057  1cc1c 4134  1 cpw1 4135   k cxpk 4174   Ins2k cins2k 4176   Ins3k cins3k 4177  kcimak 4179   SIk csik 4181   Sk cssetk 4183
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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-rex 2620  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  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  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-sik 4192  df-ssetk 4193
This theorem is referenced by:  ncfinraiselem2  4480  ncfinlowerlem1  4482  eqtfinrelk  4486  srelk  4524
  Copyright terms: Public domain W3C validator