Theorem ralbidv2 2822

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

Syntax hints:   -> wi 4   <-> wb 188   A.wal 1441   e. wcel 1886   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757

This theorem depends on definitions:  df-bi 189  df-ral 2741

This theorem is referenced by:  ralbidva  2823  ralss  3494  oneqmini  5473  ordunisuc2  6668  dfsmo2  7063  wemapsolem  8062  zorn2lem1  8923  raluz  11204  limsupgle  13528  ello12  13573  elo12  13584  lo1resb  13621  rlimresb  13622  o1resb  13623  isprm3  14626  ist1  20330  ist1-2  20356  hausdiag  20653  xkopt  20663  cnflf  21010  cnfcf  21050  metcnp  21549  caucfil  22246  mdegleb  23006  eulerpartlemgvv  29202  filnetlem4  31030  isprm7  36654  hoidmvle  38416  elbigo2  40350