Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elpwunsn Structured version   Unicode version

Theorem elpwunsn 4760
 Description: Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007.)
Assertion
Ref Expression
elpwunsn

Proof of Theorem elpwunsn
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eldif 3332 . 2
2 elpwg 3808 . . . . . . 7
3 dfss3 3340 . . . . . . 7
42, 3syl6bb 254 . . . . . 6
54notbid 287 . . . . 5
65biimpa 472 . . . 4
7 rexnal 2718 . . . 4
86, 7sylibr 205 . . 3
9 elpwi 3809 . . . . . . . . . 10
10 ssel 3344 . . . . . . . . . 10
11 elun 3490 . . . . . . . . . . . . 13
12 elsni 3840 . . . . . . . . . . . . . . 15
1312orim2i 506 . . . . . . . . . . . . . 14
1413ord 368 . . . . . . . . . . . . 13
1511, 14sylbi 189 . . . . . . . . . . . 12
1615imim2i 14 . . . . . . . . . . 11
1716imp3a 422 . . . . . . . . . 10
189, 10, 173syl 19 . . . . . . . . 9
19 eleq1 2498 . . . . . . . . . 10
2019biimpd 200 . . . . . . . . 9
2118, 20syl6 32 . . . . . . . 8
2221exp3a 427 . . . . . . 7
2322com4r 83 . . . . . 6
2423pm2.43b 49 . . . . 5
2524rexlimdv 2831 . . . 4
2625imp 420 . . 3
278, 26syldan 458 . 2
281, 27sylbi 189 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wo 359   wa 360   wceq 1653   wcel 1726  wral 2707  wrex 2708   cdif 3319   cun 3320   wss 3322  cpw 3801  csn 3816 This theorem is referenced by:  pwfilem  7404  incexclem  12621  ramub1lem1  13399  ptcmplem5  18092  onsucsuccmpi  26198 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pw 3803  df-sn 3822
 Copyright terms: Public domain W3C validator