Theorem 2rexbidv 2557

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2ralbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
2rexbidv	|- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   ps( x, y)   ch( x, y)   A( x, y)   B( x, y)

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	rexbidv 2533	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2533	1 |- ( ph -> ( E. x e. A E. y e. B ps <-> E. x e. A E. y e. B ch ) )

Syntax hints:   -> wi 4   <-> wb 105   E.wrex 2511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  f1oiso  5967  elrnmpog  6134  elrnmpo  6135  ralrnmpo  6136  rexrnmpo  6137  ovelrn  6171  eroveu  6795  genipv  7729  genpelxp  7731  genpelvl  7732  genpelvu  7733  axcnre  8101  apreap  8767  apreim  8783  aprcl  8826  aptap  8830  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  pythagtriplem19  12873  pceu  12886  pcval  12887  pczpre  12888  pcdiv  12893  4sqlem2  12980  4sqlem3  12981  4sqlem4  12983  4sqexercise2  12990  4sqlemsdc  12991  4sq  13001  znunit  14692  txuni2  14999  txbas  15001  txdis1cn  15021  elply  15477  2sqlem2  15863  2sqlem8  15871  2sqlem9  15872  upgredg  16014  3dom  16638