Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  elpwgdedVD Unicode version

Theorem elpwgdedVD 28066
Description: Membership in a power class. Theorem 86 of [Suppes] p. 47. Derived from elpwg 3632. In form of VD deduction with  ph and  ps as variable virtual hypothesis collections based on Mario Carneiro's metavariable concept. elpwgded 27703 is elpwgdedVD 28066 using conventional notation. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
elpwgdedVD.1  |-  (. ph  ->.  A  e.  _V ).
elpwgdedVD.2  |-  (. ps  ->.  A 
C_  B ).
Assertion
Ref Expression
elpwgdedVD  |-  (. (. ph ,. ps ).  ->.  A  e.  ~P B ).

Proof of Theorem elpwgdedVD
StepHypRef Expression
1 elpwgdedVD.1 . 2  |-  (. ph  ->.  A  e.  _V ).
2 elpwgdedVD.2 . 2  |-  (. ps  ->.  A 
C_  B ).
3 elpwg 3632 . . 3  |-  ( A  e.  _V  ->  ( A  e.  ~P B  <->  A 
C_  B ) )
43biimpar 471 . 2  |-  ( ( A  e.  _V  /\  A  C_  B )  ->  A  e.  ~P B
)
51, 2, 4el12 27874 1  |-  (. (. ph ,. ps ).  ->.  A  e.  ~P B ).
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788    C_ wss 3152   ~Pcpw 3625   (.wvd1 27710   (.wvhc2 27722
This theorem is referenced by:  sspwimpVD  28068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627  df-vd1 27711  df-vhc2 27723
  Copyright terms: Public domain W3C validator