Theorem 2rexbidv 2569

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 2545	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 2545	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 2523

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-rex 2528

This theorem is referenced by:  f1oiso  6005  elrnmpog  6174  elrnmpo  6175  ralrnmpo  6176  rexrnmpo  6177  ovelrn  6211  eroveu  6873  genipv  7840  genpelxp  7842  genpelvl  7843  genpelvu  7844  axcnre  8212  apreap  8878  apreim  8894  aprcl  8937  aptap  8941  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  pythagtriplem19  13005  pceu  13018  pcval  13019  pczpre  13020  pcdiv  13025  4sqlem2  13112  4sqlem3  13113  4sqlem4  13115  4sqexercise2  13122  4sqlemsdc  13123  4sq  13133  znunit  14933  txuni2  15247  txbas  15249  txdis1cn  15269  elply  15725  2sqlem2  16114  2sqlem8  16122  2sqlem9  16123  upgredg  16265  3dom  16888