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

Theorem 2ralbidva 2682
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 1626 . 2  |-  F/ x ph
2 nfv 1626 . 2  |-  F/ y
ph
3 2ralbidva.1 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
41, 2, 32ralbida 2681 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 1717   A.wral 2642
This theorem is referenced by:  disjxun  4144  isocnv3  5984  isotr  5988  f1oweALT  6006  tosso  14385  pospropd  14481  isipodrs  14507  mndpropd  14641  mhmpropd  14664  efgred  15300  cmnpropd  15341  rngpropd  15615  lmodprop2d  15926  lsspropd  16013  islmhm2  16034  lmhmpropd  16065  assapropd  16306  connsub  17398  hausdiag  17591  ist0-4  17675  ismet2  18265  txmetcnp  18460  txmetcn  18461  metuel2  18478  metucn  18483  isngp3  18509  nlmvscn  18587  ipcn  19064  iscfil2  19083  caucfil  19100  cfilresi  19112  ulmdvlem3  20178  cxpcn3  20492  ghomgsg  24876  brbtwn2  25551  colinearalglem2  25553  isbnd3b  26178  gicabl  26925  islindf4  26970  isdomn3  27185  iscvlat2N  29490  ishlat3N  29520
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2647
  Copyright terms: Public domain W3C validator