ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralnex Unicode version

Theorem ralnex 2465
Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997.)
Assertion
Ref Expression
ralnex  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )

Proof of Theorem ralnex
StepHypRef Expression
1 df-ral 2460 . 2  |-  ( A. x  e.  A  -.  ph  <->  A. x ( x  e.  A  ->  -.  ph )
)
2 alinexa 1603 . . 3  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x ( x  e.  A  /\  ph ) )
3 df-rex 2461 . . 3  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
42, 3xchbinxr 683 . 2  |-  ( A. x ( x  e.  A  ->  -.  ph )  <->  -. 
E. x  e.  A  ph )
51, 4bitri 184 1  |-  ( A. x  e.  A  -.  ph  <->  -. 
E. x  e.  A  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105   A.wal 1351   E.wex 1492    e. wcel 2148   A.wral 2455   E.wrex 2456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-ie2 1494
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-fal 1359  df-ral 2460  df-rex 2461
This theorem is referenced by:  nnral  2467  rexalim  2470  ralinexa  2504  nrex  2569  nrexdv  2570  ralnex2  2616  r19.30dc  2624  uni0b  3834  iindif2m  3954  f0rn0  5410  supmoti  6991  fodjuomnilemdc  7141  ismkvnex  7152  nninfwlpoimlemginf  7173  suprnubex  8909  icc0r  9925  ioo0  10259  ico0  10261  ioc0  10262  prmind2  12119  sqrt2irr  12161  nconstwlpolem  14782
  Copyright terms: Public domain W3C validator