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

Theorem 2ralbidva 2617
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 1610 . 2  |-  F/ x ph
2 nfv 1610 . 2  |-  F/ y
ph
3 2ralbidva.1 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
41, 2, 32ralbida 2616 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 1701   A.wral 2577
This theorem is referenced by:  disjxun  4058  isocnv3  5871  isotr  5875  f1oweALT  5893  tosso  14191  pospropd  14287  isipodrs  14313  mndpropd  14447  mhmpropd  14470  efgred  15106  cmnpropd  15147  rngpropd  15421  lmodprop2d  15736  lsspropd  15823  islmhm2  15844  lmhmpropd  15875  assapropd  16116  connsub  17203  hausdiag  17395  ist0-4  17476  ismet2  17950  txmetcnp  18145  txmetcn  18146  isngp3  18172  nlmvscn  18250  ipcn  18726  iscfil2  18745  caucfil  18762  cfilresi  18774  ulmdvlem3  19832  cxpcn3  20141  ghomgsg  24284  brbtwn2  24919  colinearalglem2  24921  isbnd3b  25657  gicabl  26411  islindf4  26456  isdomn3  26671  iscvlat2N  29332  ishlat3N  29362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-11 1732
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-ral 2582
  Copyright terms: Public domain W3C validator