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

Theorem 2ralbidva 2745
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 2744 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 2705
This theorem is referenced by:  disjxun  4210  isocnv3  6052  isotr  6056  f1oweALT  6074  tosso  14465  pospropd  14561  isipodrs  14587  mndpropd  14721  mhmpropd  14744  efgred  15380  cmnpropd  15421  rngpropd  15695  lmodprop2d  16006  lsspropd  16093  islmhm2  16114  lmhmpropd  16145  assapropd  16386  connsub  17484  hausdiag  17677  ist0-4  17761  ismet2  18363  txmetcnp  18577  txmetcn  18578  metuel2  18609  metucnOLD  18618  metucn  18619  isngp3  18645  nlmvscn  18723  ipcn  19200  iscfil2  19219  caucfil  19236  cfilresi  19248  ulmdvlem3  20318  cxpcn3  20632  isarchi2  24255  ghomgsg  25104  brbtwn2  25844  colinearalglem2  25846  isbnd3b  26494  gicabl  27240  islindf4  27285  isdomn3  27500  iscvlat2N  30122  ishlat3N  30152
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 2710
  Copyright terms: Public domain W3C validator