Theorem ralbii2 2978

Description: Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.)

Hypothesis

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

Assertion

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

Proof of Theorem ralbii2

Step	Hyp	Ref	Expression
1		ralbii2.1	. . 3 |- ( ( x e. A -> ph ) <-> ( x e. B -> ps ) )
2	1	albii 1747	. 2 |- ( A. x ( x e. A -> ph ) <-> A. x ( x e. B -> ps ) )
3		df-ral 2917	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
4		df-ral 2917	. 2 |- ( A. x e. B ps <-> A. x ( x e. B -> ps ) )
5	2, 3, 4	3bitr4i 292	1 |- ( A. x e. A ph <-> A. x e. B ps )

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

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

This theorem is referenced by:  ralbiia  2979  ralbii  2980  raleqbii  2990  ralrab  3368  raldifb  3750  raldifsni  4324  reusv2  4874  dfsup2  8350  iscard2  8802  acnnum  8875  dfac9  8958  dfacacn  8963  raluz2  11737  ralrp  11852  isprm4  15397  isdomn2  19299  isnrm2  21162  ismbl  23294  ellimc3  23643  dchrelbas2  24962  h1dei  28409  fnwe2lem2  37621  sdrgacs  37771