Theorem 2rexbidv 3057

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

Hypothesis

Ref	Expression
2rexbidv.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		2rexbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	rexbidv 3052	. 2 |- ( ph -> ( E. y e. B ps <-> E. y e. B ch ) )
3	2	rexbidv 3052	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 196   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-rex 2918

This theorem is referenced by:  f1oiso  6601  elrnmpt2g  6772  elrnmpt2  6773  ralrnmpt2  6775  ovelrn  6810  opiota  7229  omeu  7665  oeeui  7682  eroveu  7842  erov  7844  elfiun  8336  dffi3  8337  xpwdomg  8490  brdom7disj  9353  brdom6disj  9354  genpv  9821  genpelv  9822  axcnre  9985  supadd  10991  supmullem1  10993  supmullem2  10994  supmul  10995  sqrlem6  13988  ello1  14246  ello1mpt  14252  elo1  14257  lo1o1  14263  o1lo1  14268  bezoutlem1  15256  bezoutlem3  15258  bezoutlem4  15259  bezout  15260  pythagtriplem2  15522  pythagtriplem19  15538  pythagtrip  15539  pcval  15549  pceu  15551  pczpre  15552  pcdiv  15557  4sqlem2  15653  4sqlem3  15654  4sqlem4  15656  4sq  15668  vdwlem1  15685  vdwlem12  15696  vdwlem13  15697  vdwnnlem1  15699  vdwnnlem2  15700  vdwnnlem3  15701  vdwnn  15702  ramub2  15718  rami  15719  pgpfac1lem3  18476  lspprel  19094  znunit  19912  cayleyhamiltonALT  20696  hausnei  21132  isreg2  21181  txuni2  21368  txbas  21370  xkoopn  21392  txcls  21407  txcnpi  21411  txdis1cn  21438  txtube  21443  txcmplem1  21444  hausdiag  21448  tx1stc  21453  regr1lem2  21543  qustgplem  21924  met2ndci  22327  dyadmax  23366  i1fadd  23462  i1fmul  23463  elply  23951  2sqlem2  25143  2sqlem8  25151  2sqlem9  25152  2sqlem11  25154  istrkgld  25358  axtgeucl  25371  legov  25480  iscgra  25701  dfcgra2  25721  axsegconlem1  25797  axpasch  25821  axlowdim  25841  axeuclidlem  25842  nb3grpr  26284  upgr4cycl4dv4e  27045  vdgn1frgrv2  27160  fusgr2wsp2nb  27198  l2p  27331  br8d  29422  pstmval  29938  eulerpartlemgh  30440  eulerpartlemgs2  30442  cvmliftlem15  31280  cvmlift2lem10  31294  br8  31646  br6  31647  br4  31648  elaltxp  32082  brsegle  32215  ellines  32259  nn0prpwlem  32317  nn0prpw  32318  ptrest  33408  ismblfin  33450  itg2addnclem3  33463  itg2addnc  33464  isline  35025  psubspi  35033  paddfval  35083  elpadd  35085  paddvaln0N  35087  mzpcompact2lem  37314  mzpcompact2  37315  sbc4rexgOLD  37354  pell1qrval  37410  elpell1qr  37411  pell14qrval  37412  elpell14qr  37413  pell1234qrval  37414  elpell1234qr  37415  jm2.27  37575  expdiophlem1  37588  clsk1independent  38344  limclner  39883  fourierdlem42  40366  fourierdlem48  40371  isgbe  41639  isgbow  41640  isgbo  41641  sbgoldbalt  41669  sgoldbeven3prm  41671  mogoldbb  41673  sbgoldbo  41675  nnsum3primesle9  41682  sprel  41734  prelspr  41736  bigoval  42343  elbigo  42345