Theorem ralbidv2 2839

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 1734	. 2 |- ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. B -> ch ) ) )
3		df-ral 2759	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
4		df-ral 2759	. 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 1403   e. wcel 1842   A.wral 2754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725

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

This theorem is referenced by:  ralbidva  2840  ralss  3505  oneqmini  5461  ordunisuc2  6662  dfsmo2  7051  wemapsolem  8009  zorn2lem1  8908  raluz  11175  limsupgle  13449  ello12  13488  elo12  13499  lo1resb  13536  rlimresb  13537  o1resb  13538  isprm3  14435  ist1  20115  ist1-2  20141  hausdiag  20438  xkopt  20448  cnflf  20795  cnfcf  20835  metcnp  21336  caucfil  22014  mdegleb  22756  eulerpartlemgvv  28821  filnetlem4  30609  isprm7  36040  elbigo2  38683