MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2ralbidva Unicode version

Theorem 2ralbidva 2583
Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
2ralbidva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
Assertion
Ref Expression
2ralbidva  |-  ( ph  ->  ( A. x  e.  A  A. y  e.  B  ps  <->  A. x  e.  A  A. y  e.  B  ch )
)
Distinct variable groups:    x, y, ph    y, A
Allowed substitution hints:    ps( x, y)    ch( x, y)    A( x)    B( x, y)

Proof of Theorem 2ralbidva
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ph
2 nfv 1605 . 2  |-  F/ y
ph
3 2ralbidva.1 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
41, 2, 32ralbida 2582 1  |-  ( ph  ->  ( A. x  e.  A  A. y  e.  B  ps  <->  A. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1684   A.wral 2543
This theorem is referenced by:  disjxun  4021  isocnv3  5829  isotr  5833  f1oweALT  5851  tosso  14142  pospropd  14238  isipodrs  14264  mndpropd  14398  mhmpropd  14421  efgred  15057  cmnpropd  15098  rngpropd  15372  lmodprop2d  15687  lsspropd  15774  islmhm2  15795  lmhmpropd  15826  assapropd  16067  connsub  17147  hausdiag  17339  ist0-4  17420  ismet2  17898  txmetcnp  18093  txmetcn  18094  isngp3  18120  nlmvscn  18198  ipcn  18673  iscfil2  18692  caucfil  18709  cfilresi  18721  ulmdvlem3  19779  cxpcn3  20088  ghomgsg  24000  brbtwn2  24533  colinearalglem2  24535  isbnd3b  26509  gicabl  27263  islindf4  27308  isdomn3  27523  iscvlat2N  29514  ishlat3N  29544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator