Theorem ralbii 2639

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	|- (ph <-> ps)

Assertion

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

Proof of Theorem ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 |- (ph <-> ps)
2	1	a1i 10	. . 3 |- ( T. -> (ph <-> ps))
3	2	ralbidv 2635	. 2 |- ( T. -> (A.x e. A ph <-> A.x e. A ps))
4	3	trud 1323	1 |- (A.x e. A ph <-> A.x e. A ps)

Syntax hints:   <-> wb 176   T. wtru 1316  A.wral 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-ral 2620

This theorem is referenced by:  2ralbii  2641  ralinexa  2660  r3al  2672  r19.26-2  2748  r19.26-3  2749  ralbiim  2752  r19.28av  2754  r19.30  2757  r19.32v  2758  r19.35  2759  cbvral2v  2844  cbvral3v  2846  sbralie  2849  ralcom4  2878  reu8  3033  2reuswap  3039  2reu5lem2  3043  eqsn  3868  disj5  3891  uni0b  3917  uni0c  3918  ssint  3943  iuniin  3980  iuneq2  3986  iunss  4008  ssiinf  4016  iinab  4028  iinun2  4033  iindif2  4036  iinin2  4037  iinuni  4050  sspwuni  4052  iinpw  4055  evenodddisjlem1  4516  evenodddisj  4517  nnadjoinpw  4522  rexiunxp  4825  ralxpf  4828  rninxp  5061  dminxp  5062  cnviin  5119  dffun9  5136  funcnv3  5158  fncnv  5159  fnres  5200  fnopabg  5206  fnopab2g  5207  fint  5246  funimass4  5369  funconstss  5407  dff13f  5473  foov  5607  dfnnc3  5886