Theorem 2rexbidv 3203

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  f1oiso  7299  elrnmpog  7495  elrnmpo  7496  ralrnmpo  7499  ovelrn  7536  opiota  8005  omeu  8513  oeeui  8531  eroveu  8752  erov  8754  elfiun  9336  dffi3  9337  xpwdomg  9493  brdom7disj  10444  brdom6disj  10445  genpv  10913  genpelv  10914  axcnre  11078  supadd  12115  supmullem1  12117  supmullem2  12118  supmul  12119  01sqrexlem6  15200  ello1  15468  ello1mpt  15474  elo1  15479  lo1o1  15485  o1lo1  15490  bezoutlem1  16499  bezoutlem3  16501  bezoutlem4  16502  bezout  16503  pythagtriplem2  16779  pythagtriplem19  16795  pythagtrip  16796  pcval  16806  pceu  16808  pczpre  16809  pcdiv  16814  4sqlem2  16911  4sqlem3  16912  4sqlem4  16914  4sq  16926  vdwlem1  16943  vdwlem12  16954  vdwlem13  16955  vdwnnlem1  16957  vdwnnlem2  16958  vdwnnlem3  16959  vdwnn  16960  ramub2  16976  rami  16977  cat1lem  18054  cat1  18055  pgpfac1lem3  20045  lspprel  21081  znunit  21553  cayleyhamiltonALT  22866  hausnei  23303  isreg2  23352  txuni2  23540  txbas  23542  xkoopn  23564  txcls  23579  txcnpi  23583  txdis1cn  23610  txtube  23615  txcmplem1  23616  hausdiag  23620  tx1stc  23625  regr1lem2  23715  qustgplem  24096  met2ndci  24497  dyadmax  25575  i1fadd  25672  i1fmul  25673  elply  26170  2sqlem2  27395  2sqlem8  27403  2sqlem9  27404  2sqlem11  27406  elmade  27863  mulsval  28115  mulsval2lem  28116  mulsproplem9  28130  mulsproplem12  28133  sltmuls1  28153  sltmuls2  28154  mulsuniflem  28155  addsdilem2  28158  mulsasslem1  28169  mulsasslem2  28170  mulsunif2  28176  precsexlemcbv  28212  precsexlem9  28221  precsexlem11  28223  eucliddivs  28382  bdayfinbndcbv  28472  bdayfinbndlem1  28473  bdayfinbndlem2  28474  bdayfinbnd  28475  elz12s  28478  z12zsodd  28488  z12sge0  28489  remulscllem1  28506  istrkgld  28541  istrkg3ld  28543  axtgupdim2  28553  axtgeucl  28554  legov  28667  iscgra  28891  dfcgra2  28912  axsegconlem1  29000  axpasch  29024  axlowdim  29044  axeuclidlem  29045  nb3grpr  29465  upgr4cycl4dv4e  30270  vdgn1frgrv2  30381  fusgr2wsp2nb  30419  l2p  30565  br8d  32696  gsumwun  33152  constrsuc  33898  constrsslem  33901  constrconj  33905  constrllcllem  33912  constrlccllem  33913  constrcccllem  33914  constrcbvlem  33915  pstmval  34055  eulerpartlemgh  34538  eulerpartlemgs2  34540  cvmliftlem15  35496  cvmlift2lem10  35510  satf  35551  satfv0  35556  satfrnmapom  35568  satfv0fun  35569  satf0op  35575  sat1el2xp  35577  fmlafvel  35583  fmla1  35585  fmlaomn0  35588  gonan0  35590  goaln0  35591  gonar  35593  goalr  35595  fmlasucdisj  35597  satffunlem2lem1  35602  dmopab3rexdif  35603  satfv0fvfmla0  35611  sategoelfvb  35617  satfv1fvfmla1  35621  2goelgoanfmla1  35622  br8  35954  br6  35955  br4  35956  elaltxp  36173  brsegle  36306  ellines  36350  nn0prpwlem  36520  nn0prpw  36521  ptrest  37954  ismblfin  37996  itg2addnclem3  38008  itg2addnc  38009  releldmqscoss  39080  isline  40199  psubspi  40207  paddfval  40257  elpadd  40259  paddvaln0N  40261  3rspcedvd  42671  flt4lem7  43106  nna4b4nsq  43107  mzpcompact2lem  43197  mzpcompact2  43198  sbc4rexgOLD  43236  pell1qrval  43292  elpell1qr  43293  pell14qrval  43294  elpell14qr  43295  pell1234qrval  43296  elpell1234qr  43297  jm2.27  43454  expdiophlem1  43467  oenord1  43762  oaun3lem1  43820  clsk1independent  44491  limclner  46097  fourierdlem42  46595  fourierdlem48  46600  sprel  47956  prelspr  47958  prprelb  47988  prprelprb  47989  reuprpr  47995  isgbe  48239  isgbow  48240  isgbo  48241  sbgoldbalt  48269  sgoldbeven3prm  48271  mogoldbb  48273  sbgoldbo  48275  nnsum3primesle9  48282  usgrgrtrirex  48438  grlimgrtri  48491  grlimedgnedg  48619  bigoval  49037  elbigo  49039  iscnrm3r  49435  iscnrm3l  49438