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

Theorem 2ralbidva 2596
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 1609 . 2  |-  F/ x ph
2 nfv 1609 . 2  |-  F/ y
ph
3 2ralbidva.1 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
41, 2, 32ralbida 2595 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 1696   A.wral 2556
This theorem is referenced by:  disjxun  4037  isocnv3  5845  isotr  5849  f1oweALT  5867  tosso  14158  pospropd  14254  isipodrs  14280  mndpropd  14414  mhmpropd  14437  efgred  15073  cmnpropd  15114  rngpropd  15388  lmodprop2d  15703  lsspropd  15790  islmhm2  15811  lmhmpropd  15842  assapropd  16083  connsub  17163  hausdiag  17355  ist0-4  17436  ismet2  17914  txmetcnp  18109  txmetcn  18110  isngp3  18136  nlmvscn  18214  ipcn  18689  iscfil2  18708  caucfil  18725  cfilresi  18737  ulmdvlem3  19795  cxpcn3  20104  ghomgsg  24015  brbtwn2  24605  colinearalglem2  24607  isbnd3b  26612  gicabl  27366  islindf4  27411  isdomn3  27626  iscvlat2N  30136  ishlat3N  30166
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator