Theorem 2rexbidv 3201

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 3160	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3160	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

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

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 3061

This theorem is referenced by:  f1oiso  7297  elrnmpog  7493  elrnmpo  7494  ralrnmpo  7497  ovelrn  7534  opiota  8003  omeu  8512  oeeui  8530  eroveu  8749  erov  8751  elfiun  9333  dffi3  9334  xpwdomg  9490  brdom7disj  10441  brdom6disj  10442  genpv  10910  genpelv  10911  axcnre  11075  supadd  12110  supmullem1  12112  supmullem2  12113  supmul  12114  01sqrexlem6  15170  ello1  15438  ello1mpt  15444  elo1  15449  lo1o1  15455  o1lo1  15460  bezoutlem1  16466  bezoutlem3  16468  bezoutlem4  16469  bezout  16470  pythagtriplem2  16745  pythagtriplem19  16761  pythagtrip  16762  pcval  16772  pceu  16774  pczpre  16775  pcdiv  16780  4sqlem2  16877  4sqlem3  16878  4sqlem4  16880  4sq  16892  vdwlem1  16909  vdwlem12  16920  vdwlem13  16921  vdwnnlem1  16923  vdwnnlem2  16924  vdwnnlem3  16925  vdwnn  16926  ramub2  16942  rami  16943  cat1lem  18020  cat1  18021  pgpfac1lem3  20008  lspprel  21046  znunit  21518  cayleyhamiltonALT  22835  hausnei  23272  isreg2  23321  txuni2  23509  txbas  23511  xkoopn  23533  txcls  23548  txcnpi  23552  txdis1cn  23579  txtube  23584  txcmplem1  23585  hausdiag  23589  tx1stc  23594  regr1lem2  23684  qustgplem  24065  met2ndci  24466  dyadmax  25555  i1fadd  25652  i1fmul  25653  elply  26156  2sqlem2  27385  2sqlem8  27393  2sqlem9  27394  2sqlem11  27396  elmade  27853  mulsval  28105  mulsval2lem  28106  mulsproplem9  28120  mulsproplem12  28123  sltmuls1  28143  sltmuls2  28144  mulsuniflem  28145  addsdilem2  28148  mulsasslem1  28159  mulsasslem2  28160  mulsunif2  28166  precsexlemcbv  28202  precsexlem9  28211  precsexlem11  28213  eucliddivs  28372  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  bdayfinbnd  28465  elz12s  28468  z12zsodd  28478  z12sge0  28479  remulscllem1  28496  istrkgld  28531  istrkg3ld  28533  axtgupdim2  28543  axtgeucl  28544  legov  28657  iscgra  28881  dfcgra2  28902  axsegconlem1  28990  axpasch  29014  axlowdim  29034  axeuclidlem  29035  nb3grpr  29455  upgr4cycl4dv4e  30260  vdgn1frgrv2  30371  fusgr2wsp2nb  30409  l2p  30554  br8d  32686  gsumwun  33158  constrsuc  33895  constrsslem  33898  constrconj  33902  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  constrcbvlem  33912  pstmval  34052  eulerpartlemgh  34535  eulerpartlemgs2  34537  cvmliftlem15  35492  cvmlift2lem10  35506  satf  35547  satfv0  35552  satfrnmapom  35564  satfv0fun  35565  satf0op  35571  sat1el2xp  35573  fmlafvel  35579  fmla1  35581  fmlaomn0  35584  gonan0  35586  goaln0  35587  gonar  35589  goalr  35591  fmlasucdisj  35593  satffunlem2lem1  35598  dmopab3rexdif  35599  satfv0fvfmla0  35607  sategoelfvb  35613  satfv1fvfmla1  35617  2goelgoanfmla1  35618  br8  35950  br6  35951  br4  35952  elaltxp  36169  brsegle  36302  ellines  36346  nn0prpwlem  36516  nn0prpw  36517  ptrest  37820  ismblfin  37862  itg2addnclem3  37874  itg2addnc  37875  releldmqscoss  38919  isline  39999  psubspi  40007  paddfval  40057  elpadd  40059  paddvaln0N  40061  3rspcedvd  42472  flt4lem7  42902  nna4b4nsq  42903  mzpcompact2lem  42993  mzpcompact2  42994  sbc4rexgOLD  43032  pell1qrval  43088  elpell1qr  43089  pell14qrval  43090  elpell14qr  43091  pell1234qrval  43092  elpell1234qr  43093  jm2.27  43250  expdiophlem1  43263  oenord1  43558  oaun3lem1  43616  clsk1independent  44287  limclner  45895  fourierdlem42  46393  fourierdlem48  46398  sprel  47730  prelspr  47732  prprelb  47762  prprelprb  47763  reuprpr  47769  isgbe  47997  isgbow  47998  isgbo  47999  sbgoldbalt  48027  sgoldbeven3prm  48029  mogoldbb  48031  sbgoldbo  48033  nnsum3primesle9  48040  usgrgrtrirex  48196  grlimgrtri  48249  grlimedgnedg  48377  bigoval  48795  elbigo  48797  iscnrm3r  49193  iscnrm3l  49196