Theorem ralbii2 2817

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

Syntax hints:   -> wi 4   <-> wb 188   A.wal 1442   e. wcel 1887   A.wral 2737

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

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

This theorem is referenced by:  ralbiia  2818  ralbii  2819  raleqbii  2833  ralrab  3200  raldifb  3573  raldifsni  4102  reusv2  4609  dfsup2  7958  iscard2  8410  acnnum  8483  dfac9  8566  dfacacn  8571  raluz2  11208  ralrp  11321  isprm4  14634  isdomn2  18523  isnrm2  20374  ismbl  22480  ellimc3  22834  dchrelbas2  24165  h1dei  27203  fnwe2lem2  35909  sdrgacs  36067