Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-exnalimn Structured version   Unicode version

Theorem bj-exnalimn 30798
Description: A transformation of quantifiers and logical connectives. The general statement that equs3 1760 proves.

This and the following theorems are the general instances of already proved theorems. They could be moved to the main part, before ax-5 1727. I propose to move to the main part: bj-exnalimn 30798, bj-exaleximi 30801, bj-exalimi 30802, bj-ax12i 30803, bj-ax12wlem 30805. A new label is needed for bj-ax12i 30803 and label suggestions are welcome for the others. I also propose to change  -.  A. x -. to  E. x in speimfw 1761 and spimfw 1763 (other spim* theorems use 
E. x and very very few theorems in set.mm use  -.  A. x -.). (Contributed by BJ, 29-Sep-2019.)

Assertion
Ref Expression
bj-exnalimn  |-  ( E. x ( ph  /\  ps )  <->  -.  A. x
( ph  ->  -.  ps ) )

Proof of Theorem bj-exnalimn
StepHypRef Expression
1 alinexa 1686 . 2  |-  ( A. x ( ph  ->  -. 
ps )  <->  -.  E. x
( ph  /\  ps )
)
21con2bii 332 1  |-  ( E. x ( ph  /\  ps )  <->  -.  A. x
( ph  ->  -.  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 186    /\ wa 369   A.wal 1405   E.wex 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654
This theorem depends on definitions:  df-bi 187  df-an 371  df-ex 1636
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator