Theorem ralbidv2 2756

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 1679	. 2 |- ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
3		df-ral 2739	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
4		df-ral 2739	. 2 |- ( A. x e. B ch <-> A. x ( x e. B -> ch ) )
5	2, 3, 4	3bitr4g 288	1 |- ( ph -> ( A. x e. A ps <-> A. x e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1367   e. wcel 1756   A.wral 2734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670

This theorem depends on definitions:  df-bi 185  df-ral 2739

This theorem is referenced by:  ralss  3437  oneqmini  4789  ordunisuc2  6474  dfsmo2  6827  wemapsolem  7783  zorn2lem1  8684  raluz  10922  limsupgle  12974  ello12  13013  elo12  13024  lo1resb  13061  rlimresb  13062  o1resb  13063  isprm3  13791  ist1  18944  ist1-2  18970  hausdiag  19237  xkopt  19247  cnflf  19594  cnfcf  19634  metcnp  20135  caucfil  20813  mdegleb  21554  eulerpartlemgvv  26778  filnetlem4  28625