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

Theorem ralrimivva 2444
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
ralrimivva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ps )
Assertion
Ref Expression
ralrimivva  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Distinct variable groups:    ph, x, y   
y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ps )
21ex 113 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2443 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1434   A.wral 2349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354
This theorem is referenced by:  swopo  4069  sosng  4439  fcof1  5454  fliftfund  5468  isoresbr  5480  isocnv  5482  f1oiso  5496  caovclg  5684  caovcomg  5687  off  5755  caofrss  5766  fmpt2co  5868  poxp  5884  f1od2  5887  eroprf  6265  dom2lem  6319  xpf1o  6385  nnwetri  6436  supmoti  6465  supsnti  6477  supisoti  6482  addlocpr  6788  mullocpr  6823  cauappcvgprlemloc  6904  cauappcvgprlemlim  6913  caucvgprlemloc  6927  caucvgprprlemloc  6955  rereceu  7117  cju  8105  exbtwnz  9337  frec2uzf1od  9488  frec2uzisod  9489  frecuzrdgrrn  9490  frec2uzrdg  9491  frecuzrdgrcl  9492  frecuzrdgsuc  9496  frecuzrdgrclt  9497  frecuzrdgg  9498  frecuzrdgsuctlem  9505  iseqoveq  9540  iseqcaopr3  9556  iseqcaopr2  9557  iseqhomo  9565  iseqdistr  9567  rsqrmo  10051  climcn2  10286  addcn2  10287  mulcn2  10289  divalglemeunn  10465  divalglemeuneg  10467  bezoutlemeu  10540  isprm6  10670  pw2dvdseu  10690
  Copyright terms: Public domain W3C validator