Theorem 2ralbidva 2901

Description: Formula-building rule for restricted universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.)

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		2ralbidva.1	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( ps <-> ch ) )
2	1	anassrs 648	. . 3 |- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( ps <-> ch ) )
3	2	ralbidva 2895	. 2 |- ( ( ph /\ x e. A ) -> ( A. y e. B ps <-> A. y e. B ch ) )
4	3	ralbidva 2895	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 1762   A.wral 2809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675

This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2814

This theorem is referenced by:  disjxun  4440  isocnv3  6209  isotr  6213  f1oweALT  6760  fnmpt2ovd  6853  tosso  15514  pospropd  15612  isipodrs  15639  mndpropd  15754  mhmpropd  15778  efgred  16557  cmnpropd  16598  rngpropd  17012  lmodprop2d  17350  lsspropd  17441  islmhm2  17462  lmhmpropd  17497  assapropd  17742  islindf4  18635  scmatmats  18775  cpmatel2  18976  1elcpmat  18978  m2cpminvid2  19018  decpmataa0  19031  pmatcollpw2lem  19040  connsub  19683  hausdiag  19876  ist0-4  19960  ismet2  20566  txmetcnp  20780  txmetcn  20781  metuel2  20812  metucnOLD  20821  metucn  20822  isngp3  20848  nlmvscn  20926  ipcn  21416  iscfil2  21435  caucfil  21452  cfilresi  21464  ulmdvlem3  22526  cxpcn3  22845  perpcom  23793  brbtwn2  23879  colinearalglem2  23881  eengtrkg  23959  isarchi2  27379  ghomgsg  28496  isbnd3b  29873  gicabl  30642  isdomn3  30760  lindslinindsimp2  32014  iscvlat2N  33998  ishlat3N  34028