Theorem ralbii 2638

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 2634	. 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 2614

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 2619

This theorem is referenced by:  2ralbii  2640  ralinexa  2659  r3al  2671  r19.26-2  2747  r19.26-3  2748  ralbiim  2751  r19.28av  2753  r19.30  2756  r19.32v  2757  r19.35  2758  cbvral2v  2843  cbvral3v  2845  sbralie  2848  ralcom4  2877  reu8  3032  2reuswap  3038  2reu5lem2  3042  eqsn  3867  disj5  3890  uni0b  3916  uni0c  3917  ssint  3942  iuniin  3979  iuneq2  3985  iunss  4007  ssiinf  4015  iinab  4027  iinun2  4032  iindif2  4035  iinin2  4036  iinuni  4049  sspwuni  4051  iinpw  4054  evenodddisjlem1  4515  evenodddisj  4516  nnadjoinpw  4521  rexiunxp  4824  ralxpf  4827  rninxp  5060  dminxp  5061  cnviin  5118  dffun9  5135  funcnv3  5157  fncnv  5158  fnres  5199  fnopabg  5205  fnopab2g  5206  fint  5245  funimass4  5368  funconstss  5406  dff13f  5472  foov  5606  dfnnc3  5885