Theorem ralbidv2 2984

Description: Formula-building rule for restricted universal quantifier (deduction rule). (Contributed by NM, 6-Apr-1997.)

Hypothesis

Ref	Expression
ralbidv2.1	|- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )

Assertion

Ref	Expression
ralbidv2	|- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)   B( x)

Proof of Theorem ralbidv2

Step	Hyp	Ref	Expression
1		ralbidv2.1	. . 3 |- ( ph -> ( ( x e. A -> ps ) <-> ( x e. B -> ch ) ) )
2	1	albidv 1849	. 2 |- ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
3		df-ral 2917	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
4		df-ral 2917	. 2 |- ( A. x e. B ch <-> A. x ( x e. B -> ch ) )
5	2, 3, 4	3bitr4g 303	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralbidva  2985  ralss  3668  oneqmini  5776  ordunisuc2  7044  dfsmo2  7444  wemapsolem  8455  zorn2lem1  9318  raluz  11736  limsupgle  14208  ello12  14247  elo12  14258  lo1resb  14295  rlimresb  14296  o1resb  14297  isprm3  15396  isprm7  15420  ist1  21125  ist1-2  21151  hausdiag  21448  xkopt  21458  cnflf  21806  cnfcf  21846  metcnp  22346  caucfil  23081  mdegleb  23824  eulerpartlemgvv  30438  filnetlem4  32376  hoidmvle  40814  elbigo2  42346