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

Theorem ralrimivva 2455
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 2454 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 1438   A.wral 2359
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  swopo  4124  sosng  4499  fcof1  5544  fliftfund  5558  isoresbr  5570  isocnv  5572  f1oiso  5587  caovclg  5779  caovcomg  5782  off  5850  caofrss  5861  fmpt2co  5963  poxp  5979  f1od2  5982  eroprf  6365  dom2lem  6469  xpf1o  6540  fidifsnid  6567  nnwetri  6606  undiffi  6615  fidcenumlemim  6640  supmoti  6667  supsnti  6679  supisoti  6684  addlocpr  7074  mullocpr  7109  cauappcvgprlemloc  7190  cauappcvgprlemlim  7199  caucvgprlemloc  7213  caucvgprprlemloc  7241  rereceu  7403  cju  8393  exbtwnz  9627  frec2uzf1od  9778  frec2uzisod  9779  frecuzrdgrrn  9780  frec2uzrdg  9781  frecuzrdgrcl  9782  frecuzrdgsuc  9786  frecuzrdgrclt  9787  frecuzrdgg  9788  frecuzrdgsuctlem  9795  iseqoveq  9850  iseqcaopr3  9875  iseqcaopr2  9876  iseqf1olemqf1o  9887  iseqhomo  9907  seq3homo  9909  iseqdistr  9910  seq3distr  9911  fimaxq  10200  zfz1isolem1  10210  rsqrmo  10425  climcn2  10662  addcn2  10663  mulcn2  10665  fsum2dlemstep  10791  fisumcom2  10795  divalglemeunn  11003  divalglemeuneg  11005  bezoutlemeu  11078  isprm6  11208  pw2dvdseu  11228  crth  11282  exmidsbthrlem  11558
  Copyright terms: Public domain W3C validator