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

Theorem 2ralbidva 2752
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 1631 . 2  |-  F/ x ph
2 nfv 1631 . 2  |-  F/ y
ph
3 2ralbidva.1 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
41, 2, 32ralbida 2751 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 178    /\ wa 360    e. wcel 1728   A.wral 2712
This theorem is referenced by:  disjxun  4241  isocnv3  6088  isotr  6092  f1oweALT  6110  tosso  14503  pospropd  14599  isipodrs  14625  mndpropd  14759  mhmpropd  14782  efgred  15418  cmnpropd  15459  rngpropd  15733  lmodprop2d  16044  lsspropd  16131  islmhm2  16152  lmhmpropd  16183  assapropd  16424  connsub  17522  hausdiag  17715  ist0-4  17799  ismet2  18401  txmetcnp  18615  txmetcn  18616  metuel2  18647  metucnOLD  18656  metucn  18657  isngp3  18683  nlmvscn  18761  ipcn  19238  iscfil2  19257  caucfil  19274  cfilresi  19286  ulmdvlem3  20356  cxpcn3  20670  isarchi2  24290  ghomgsg  25139  brbtwn2  25879  colinearalglem2  25881  isbnd3b  26536  gicabl  27352  islindf4  27397  isdomn3  27612  iscvlat2N  30296  ishlat3N  30326
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-11 1764
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2717
  Copyright terms: Public domain W3C validator