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

Theorem r19.28zv 3763
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 3761 . . 3  |-  ( A  =/=  (/)  ->  ( ph  <->  A. x  e.  A  ph ) )
21anbi1d 697 . 2  |-  ( A  =/=  (/)  ->  ( ( ph  /\  A. x  e.  A  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) ) )
3 r19.26 2839 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
42, 3syl6rbbr 264 1  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  ( ph  /\  ps )  <->  ( ph  /\ 
A. x  e.  A  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    =/= wne 2596   A.wral 2705   (/)c0 3625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-v 2964  df-dif 3319  df-nul 3626
This theorem is referenced by:  raaanv  3776  raltpd  3986  iinrab  4220  iindif2  4227  iinin2  4228  reusv2lem5  4485  reusv7OLD  4492  xpiindi  4962  fint  5578  ixpiin  7277  neips  18558  txflf  19420  dfpo2  27411  diaglbN  34270  dihglbcpreN  34515
  Copyright terms: Public domain W3C validator