Theorem ralbidv2 2892

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 1684	. 2 |- ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
3		df-ral 2812	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
4		df-ral 2812	. 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 1372   e. wcel 1762   A.wral 2807

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-ral 2812

This theorem is referenced by:  ralbidva  2893  ralss  3559  oneqmini  4922  ordunisuc2  6650  dfsmo2  7008  wemapsolem  7964  zorn2lem1  8865  raluz  11118  limsupgle  13249  ello12  13288  elo12  13299  lo1resb  13336  rlimresb  13337  o1resb  13338  isprm3  14074  ist1  19581  ist1-2  19607  hausdiag  19874  xkopt  19884  cnflf  20231  cnfcf  20271  metcnp  20772  caucfil  21450  mdegleb  22192  eulerpartlemgvv  27941  filnetlem4  29789