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

Theorem ralrimivv 2558
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by NM, 24-Jul-2004.)
Hypothesis
Ref Expression
ralrimivv.1  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
Assertion
Ref Expression
ralrimivv  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Distinct variable groups:    x, y, ph    y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem ralrimivv
StepHypRef Expression
1 ralrimivv.1 . . . 4  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
21expd 258 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( y  e.  B  ->  ps ) ) )
32ralrimdv 2556 . 2  |-  ( ph  ->  ( x  e.  A  ->  A. y  e.  B  ps ) )
43ralrimiv 2549 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    e. wcel 2148   A.wral 2455
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-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460
This theorem is referenced by:  ralrimivva  2559  ralrimdvv  2561  reuind  2942  ssrel2  4716  f1o2ndf1  6228  smoiso  6302  nndifsnid  6507  receuap  8625  lbreu  8901  0subm  12870  insubm  12871  iscmnd  13099  tgcl  13500  topbas  13503  epttop  13526  restbasg  13604  txbas  13694  txbasval  13703  blfps  13845  blf  13846  blbas  13869
  Copyright terms: Public domain W3C validator