Theorem 2rexbidv 2533

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-rex 2492

This theorem is referenced by:  f1oiso  5918  elrnmpog  6081  elrnmpo  6082  ralrnmpo  6083  rexrnmpo  6084  ovelrn  6118  eroveu  6736  genipv  7657  genpelxp  7659  genpelvl  7660  genpelvu  7661  axcnre  8029  apreap  8695  apreim  8711  aprcl  8754  aptap  8758  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  pythagtriplem19  12720  pceu  12733  pcval  12734  pczpre  12735  pcdiv  12740  4sqlem2  12827  4sqlem3  12828  4sqlem4  12830  4sqexercise2  12837  4sqlemsdc  12838  4sq  12848  znunit  14536  txuni2  14843  txbas  14845  txdis1cn  14865  elply  15321  2sqlem2  15707  2sqlem8  15715  2sqlem9  15716  upgredg  15848