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

Theorem r19.28zv 3455
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 3453 . . 3  |-  ( A  =/=  (/)  ->  ( ph  <->  A. x  e.  A  ph ) )
21anbi1d 688 . 2  |-  ( A  =/=  (/)  ->  ( ( ph  /\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) ) )
3 r19.26 2637 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
42, 3syl6rbbr 257 1  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  ( ph  /\  ps )  <->  ( ph  /\ 
A. x  e.  A  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    =/= wne 2412   A.wral 2509   (/)c0 3362
This theorem is referenced by:  raaanv  3468  iinrab  3862  iindif2  3869  iinin2  3870  reusv2lem5  4430  reusv7OLD  4437  xpiindi  4728  fint  5277  ixpiin  6728  neips  16682  txflf  17533  dfpo2  23282  diaglbN  30149  dihglbcpreN  30394
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-v 2729  df-dif 3081  df-nul 3363
  Copyright terms: Public domain W3C validator