Theorem ralbii2 2694

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 1572	. 2 |- ( A. x ( x e. A -> ph ) <-> A. x ( x e. B -> ps ) )
3		df-ral 2671	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
4		df-ral 2671	. 2 |- ( A. x e. B ps <-> A. x ( x e. B -> ps ) )
5	2, 3, 4	3bitr4i 269	1 |- ( A. x e. A ph <-> A. x e. B ps )

Syntax hints:   -> wi 4   <-> wb 177   A.wal 1546   e. wcel 1721   A.wral 2666

This theorem is referenced by:  raleqbii  2696  ralbiia  2698  ralrab  3056  raldifb  3447  reusv2  4688  dfsup2  7405  iscard2  7819  acnnum  7889  dfac9  7972  dfacacn  7977  raluz2  10482  ralrp  10586  isprm4  13044  isdomn2  16314  isnrm2  17376  ismbl  19375  ellimc3  19719  dchrelbas2  20974  h1dei  23005  raldifsni  26624  fnwe2lem2  27016  sdrgacs  27377

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563

This theorem depends on definitions:  df-bi 178  df-ral 2671