MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.28zv Unicode version

Theorem r19.28zv 3687
Description: Restricted quantifier version of Theorem 19.28 of [Margaris] p. 90. It is valid only when the domain of quantification is not empty. (Contributed by NM, 19-Aug-2004.)
Assertion
Ref Expression
r19.28zv  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  ( ph  /\  ps )  <->  ( ph  /\ 
A. x  e.  A  ps ) ) )
Distinct variable groups:    x, A    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem r19.28zv
StepHypRef Expression
1 r19.3rzv 3685 . . 3  |-  ( A  =/=  (/)  ->  ( ph  <->  A. x  e.  A  ph ) )
21anbi1d 686 . 2  |-  ( A  =/=  (/)  ->  ( ( ph  /\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) ) )
3 r19.26 2802 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
42, 3syl6rbbr 256 1  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  ( ph  /\  ps )  <->  ( ph  /\ 
A. x  e.  A  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    =/= wne 2571   A.wral 2670   (/)c0 3592
This theorem is referenced by:  raaanv  3700  iinrab  4117  iindif2  4124  iinin2  4125  reusv2lem5  4691  reusv7OLD  4698  xpiindi  4973  fint  5585  ixpiin  7051  neips  17136  txflf  17995  dfpo2  25330  diaglbN  31542  dihglbcpreN  31787
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-v 2922  df-dif 3287  df-nul 3593
  Copyright terms: Public domain W3C validator