Theorem 2rexbidv 2502

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  f1oiso  5827  elrnmpog  5987  elrnmpo  5988  ralrnmpo  5989  rexrnmpo  5990  ovelrn  6023  eroveu  6626  genipv  7508  genpelxp  7510  genpelvl  7511  genpelvu  7512  axcnre  7880  apreap  8544  apreim  8560  aprcl  8603  aptap  8607  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  pythagtriplem19  12282  pceu  12295  pcval  12296  pczpre  12297  pcdiv  12302  4sqlem2  12387  4sqlem3  12388  4sqlem4  12390  txuni2  13759  txbas  13761  txdis1cn  13781  2sqlem2  14465  2sqlem8  14473  2sqlem9  14474