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

Step	Hyp	Ref	Expression
1		nfv 1672	. 2 |- F/ x ph
2		nfv 1672	. 2 |- F/ y ph
3		2ralbidva.1	. 2 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )
4	1, 2, 3	2ralbida 2744	1 |- ( ph -> ( A. x e. A A. y e. B ps <-> A. x e. A A. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1755   A.wral 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710

This theorem is referenced by:  disjxun  4278  isocnv3  6010  isotr  6014  f1oweALT  6550  fnmpt2ovd  6640  tosso  15189  pospropd  15287  isipodrs  15314  mndpropd  15429  mhmpropd  15453  efgred  16225  cmnpropd  16266  rngpropd  16612  lmodprop2d  16931  lsspropd  17020  islmhm2  17041  lmhmpropd  17076  assapropd  17320  islindf4  18109  connsub  18867  hausdiag  19060  ist0-4  19144  ismet2  19750  txmetcnp  19964  txmetcn  19965  metuel2  19996  metucnOLD  20005  metucn  20006  isngp3  20032  nlmvscn  20110  ipcn  20600  iscfil2  20619  caucfil  20636  cfilresi  20648  ulmdvlem3  21752  cxpcn3  22071  brbtwn2  22974  colinearalglem2  22976  eengtrkg  23054  isarchi2  26026  ghomgsg  27159  isbnd3b  28528  gicabl  29299  isdomn3  29417  lindslinindsimp2  30706  iscvlat2N  32542  ishlat3N  32572