Theorem ralbii2 2741

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

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1362   e. wcel 1761   A.wral 2713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607

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

This theorem is referenced by:  raleqbii  2743  ralbiia  2745  ralrab  3118  raldifb  3493  raldifsni  4002  reusv2  4495  dfsup2  7688  iscard2  8142  acnnum  8218  dfac9  8301  dfacacn  8306  raluz2  10900  ralrp  11005  isprm4  13769  isdomn2  17349  isnrm2  18921  ismbl  20968  ellimc3  21313  dchrelbas2  22535  h1dei  24888  fnwe2lem2  29329  sdrgacs  29483