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

Theorem 2ralbidva 2732
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 1629 . 2  |-  F/ x ph
2 nfv 1629 . 2  |-  F/ y
ph
3 2ralbidva.1 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
41, 2, 32ralbida 2731 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 177    /\ wa 359    e. wcel 1725   A.wral 2692
This theorem is referenced by:  disjxun  4197  isocnv3  6038  isotr  6042  f1oweALT  6060  tosso  14448  pospropd  14544  isipodrs  14570  mndpropd  14704  mhmpropd  14727  efgred  15363  cmnpropd  15404  rngpropd  15678  lmodprop2d  15989  lsspropd  16076  islmhm2  16097  lmhmpropd  16128  assapropd  16369  connsub  17467  hausdiag  17660  ist0-4  17744  ismet2  18346  txmetcnp  18560  txmetcn  18561  metuel2  18592  metucnOLD  18601  metucn  18602  isngp3  18628  nlmvscn  18706  ipcn  19183  iscfil2  19202  caucfil  19219  cfilresi  19231  ulmdvlem3  20301  cxpcn3  20615  isarchi2  24238  ghomgsg  25087  brbtwn2  25787  colinearalglem2  25789  isbnd3b  26426  gicabl  27173  islindf4  27218  isdomn3  27433  iscvlat2N  29853  ishlat3N  29883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2697
  Copyright terms: Public domain W3C validator