Theorem 2rexbidv 3199

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

Hypothesis

Ref	Expression
2ralbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2ralbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	rexbidv 3158	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3158	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  f1oiso  7295  elrnmpog  7491  elrnmpo  7492  ralrnmpo  7495  ovelrn  7532  opiota  8001  omeu  8510  oeeui  8528  eroveu  8747  erov  8749  elfiun  9331  dffi3  9332  xpwdomg  9488  brdom7disj  10439  brdom6disj  10440  genpv  10908  genpelv  10909  axcnre  11073  supadd  12108  supmullem1  12110  supmullem2  12111  supmul  12112  01sqrexlem6  15168  ello1  15436  ello1mpt  15442  elo1  15447  lo1o1  15453  o1lo1  15458  bezoutlem1  16464  bezoutlem3  16466  bezoutlem4  16467  bezout  16468  pythagtriplem2  16743  pythagtriplem19  16759  pythagtrip  16760  pcval  16770  pceu  16772  pczpre  16773  pcdiv  16778  4sqlem2  16875  4sqlem3  16876  4sqlem4  16878  4sq  16890  vdwlem1  16907  vdwlem12  16918  vdwlem13  16919  vdwnnlem1  16921  vdwnnlem2  16922  vdwnnlem3  16923  vdwnn  16924  ramub2  16940  rami  16941  cat1lem  18018  cat1  18019  pgpfac1lem3  20006  lspprel  21044  znunit  21516  cayleyhamiltonALT  22833  hausnei  23270  isreg2  23319  txuni2  23507  txbas  23509  xkoopn  23531  txcls  23546  txcnpi  23550  txdis1cn  23577  txtube  23582  txcmplem1  23583  hausdiag  23587  tx1stc  23592  regr1lem2  23682  qustgplem  24063  met2ndci  24464  dyadmax  25553  i1fadd  25650  i1fmul  25651  elply  26154  2sqlem2  27383  2sqlem8  27391  2sqlem9  27392  2sqlem11  27394  elmade  27839  mulsval  28078  mulsval2lem  28079  mulsproplem9  28093  mulsproplem12  28096  ssltmul1  28116  ssltmul2  28117  mulsuniflem  28118  addsdilem2  28121  mulsasslem1  28132  mulsasslem2  28133  mulsunif2  28139  precsexlemcbv  28174  precsexlem9  28183  precsexlem11  28185  eucliddivs  28334  elzs12  28421  zs12zodd  28431  zs12ge0  28432  remulscllem1  28445  istrkgld  28480  istrkg3ld  28482  axtgupdim2  28492  axtgeucl  28493  legov  28606  iscgra  28830  dfcgra2  28851  axsegconlem1  28939  axpasch  28963  axlowdim  28983  axeuclidlem  28984  nb3grpr  29404  upgr4cycl4dv4e  30209  vdgn1frgrv2  30320  fusgr2wsp2nb  30358  l2p  30503  br8d  32635  gsumwun  33107  constrsuc  33844  constrsslem  33847  constrconj  33851  constrllcllem  33858  constrlccllem  33859  constrcccllem  33860  constrcbvlem  33861  pstmval  34001  eulerpartlemgh  34484  eulerpartlemgs2  34486  cvmliftlem15  35441  cvmlift2lem10  35455  satf  35496  satfv0  35501  satfrnmapom  35513  satfv0fun  35514  satf0op  35520  sat1el2xp  35522  fmlafvel  35528  fmla1  35530  fmlaomn0  35533  gonan0  35535  goaln0  35536  gonar  35538  goalr  35540  fmlasucdisj  35542  satffunlem2lem1  35547  dmopab3rexdif  35548  satfv0fvfmla0  35556  sategoelfvb  35562  satfv1fvfmla1  35566  2goelgoanfmla1  35567  br8  35899  br6  35900  br4  35901  elaltxp  36118  brsegle  36251  ellines  36295  nn0prpwlem  36465  nn0prpw  36466  ptrest  37759  ismblfin  37801  itg2addnclem3  37813  itg2addnc  37814  releldmqscoss  38858  isline  39938  psubspi  39946  paddfval  39996  elpadd  39998  paddvaln0N  40000  3rspcedvd  42413  flt4lem7  42844  nna4b4nsq  42845  mzpcompact2lem  42935  mzpcompact2  42936  sbc4rexgOLD  42974  pell1qrval  43030  elpell1qr  43031  pell14qrval  43032  elpell14qr  43033  pell1234qrval  43034  elpell1234qr  43035  jm2.27  43192  expdiophlem1  43205  oenord1  43500  oaun3lem1  43558  clsk1independent  44229  limclner  45837  fourierdlem42  46335  fourierdlem48  46340  sprel  47672  prelspr  47674  prprelb  47704  prprelprb  47705  reuprpr  47711  isgbe  47939  isgbow  47940  isgbo  47941  sbgoldbalt  47969  sgoldbeven3prm  47971  mogoldbb  47973  sbgoldbo  47975  nnsum3primesle9  47982  usgrgrtrirex  48138  grlimgrtri  48191  grlimedgnedg  48319  bigoval  48737  elbigo  48739  iscnrm3r  49135  iscnrm3l  49138