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  7300  elrnmpog  7496  elrnmpo  7497  ralrnmpo  7500  ovelrn  7537  opiota  8006  omeu  8514  oeeui  8532  eroveu  8753  erov  8755  elfiun  9337  dffi3  9338  xpwdomg  9494  brdom7disj  10447  brdom6disj  10448  genpv  10916  genpelv  10917  axcnre  11081  supadd  12118  supmullem1  12120  supmullem2  12121  supmul  12122  01sqrexlem6  15203  ello1  15471  ello1mpt  15477  elo1  15482  lo1o1  15488  o1lo1  15493  bezoutlem1  16502  bezoutlem3  16504  bezoutlem4  16505  bezout  16506  pythagtriplem2  16782  pythagtriplem19  16798  pythagtrip  16799  pcval  16809  pceu  16811  pczpre  16812  pcdiv  16817  4sqlem2  16914  4sqlem3  16915  4sqlem4  16917  4sq  16929  vdwlem1  16946  vdwlem12  16957  vdwlem13  16958  vdwnnlem1  16960  vdwnnlem2  16961  vdwnnlem3  16962  vdwnn  16963  ramub2  16979  rami  16980  cat1lem  18057  cat1  18058  pgpfac1lem3  20048  lspprel  21084  znunit  21556  cayleyhamiltonALT  22869  hausnei  23306  isreg2  23355  txuni2  23543  txbas  23545  xkoopn  23567  txcls  23582  txcnpi  23586  txdis1cn  23613  txtube  23618  txcmplem1  23619  hausdiag  23623  tx1stc  23628  regr1lem2  23718  qustgplem  24099  met2ndci  24500  dyadmax  25578  i1fadd  25675  i1fmul  25676  elply  26173  2sqlem2  27398  2sqlem8  27406  2sqlem9  27407  2sqlem11  27409  elmade  27866  mulsval  28118  mulsval2lem  28119  mulsproplem9  28133  mulsproplem12  28136  sltmuls1  28156  sltmuls2  28157  mulsuniflem  28158  addsdilem2  28161  mulsasslem1  28172  mulsasslem2  28173  mulsunif2  28179  precsexlemcbv  28215  precsexlem9  28224  precsexlem11  28226  eucliddivs  28385  bdayfinbndcbv  28475  bdayfinbndlem1  28476  bdayfinbndlem2  28477  bdayfinbnd  28478  elz12s  28481  z12zsodd  28491  z12sge0  28492  remulscllem1  28509  istrkgld  28544  istrkg3ld  28546  axtgupdim2  28556  axtgeucl  28557  legov  28670  iscgra  28894  dfcgra2  28915  axsegconlem1  29003  axpasch  29027  axlowdim  29047  axeuclidlem  29048  nb3grpr  29468  upgr4cycl4dv4e  30273  vdgn1frgrv2  30384  fusgr2wsp2nb  30422  l2p  30568  br8d  32699  gsumwun  33155  constrsuc  33901  constrsslem  33904  constrconj  33908  constrllcllem  33915  constrlccllem  33916  constrcccllem  33917  constrcbvlem  33918  pstmval  34058  eulerpartlemgh  34541  eulerpartlemgs2  34543  cvmliftlem15  35499  cvmlift2lem10  35513  satf  35554  satfv0  35559  satfrnmapom  35571  satfv0fun  35572  satf0op  35578  sat1el2xp  35580  fmlafvel  35586  fmla1  35588  fmlaomn0  35591  gonan0  35593  goaln0  35594  gonar  35596  goalr  35598  fmlasucdisj  35600  satffunlem2lem1  35605  dmopab3rexdif  35606  satfv0fvfmla0  35614  sategoelfvb  35620  satfv1fvfmla1  35624  2goelgoanfmla1  35625  br8  35957  br6  35958  br4  35959  elaltxp  36176  brsegle  36309  ellines  36353  nn0prpwlem  36523  nn0prpw  36524  ptrest  37957  ismblfin  37999  itg2addnclem3  38011  itg2addnc  38012  releldmqscoss  39083  isline  40202  psubspi  40210  paddfval  40260  elpadd  40262  paddvaln0N  40264  3rspcedvd  42674  flt4lem7  43109  nna4b4nsq  43110  mzpcompact2lem  43200  mzpcompact2  43201  sbc4rexgOLD  43239  pell1qrval  43295  elpell1qr  43296  pell14qrval  43297  elpell14qr  43298  pell1234qrval  43299  elpell1234qr  43300  jm2.27  43457  expdiophlem1  43470  oenord1  43765  oaun3lem1  43823  clsk1independent  44494  limclner  46100  fourierdlem42  46598  fourierdlem48  46603  sprel  47959  prelspr  47961  prprelb  47991  prprelprb  47992  reuprpr  47998  isgbe  48242  isgbow  48243  isgbo  48244  sbgoldbalt  48272  sgoldbeven3prm  48274  mogoldbb  48276  sbgoldbo  48278  nnsum3primesle9  48285  usgrgrtrirex  48441  grlimgrtri  48494  grlimedgnedg  48622  bigoval  49040  elbigo  49042  iscnrm3r  49438  iscnrm3l  49441