Theorem 2rexbidv 3204

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

Syntax hints:   → wi 4   ↔ wb 207  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  f1oiso  7295  elrnmpog  7491  elrnmpo  7492  ralrnmpo  7495  ovelrn  7532  opiota  8001  omeu  8510  oeeui  8528  eroveu  8749  erov  8751  elfiun  9333  dffi3  9334  xpwdomg  9490  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  21084  znunit  21538  cayleyhamiltonALT  22874  hausnei  23311  isreg2  23360  txuni2  23548  txbas  23550  xkoopn  23572  txcls  23587  txcnpi  23591  txdis1cn  23618  txtube  23623  txcmplem1  23624  hausdiag  23628  tx1stc  23633  regr1lem2  23723  qustgplem  24104  met2ndci  24505  dyadmax  25583  i1fadd  25680  i1fmul  25681  elply  26178  2sqlem2  27399  2sqlem8  27407  2sqlem9  27408  2sqlem11  27410  elmade  27867  mulsval  28119  mulsval2lem  28120  mulsproplem9  28134  mulsproplem12  28137  sltmuls1  28157  sltmuls2  28158  mulsuniflem  28159  addsdilem2  28162  mulsasslem1  28173  mulsasslem2  28174  mulsunif2  28180  precsexlemcbv  28216  precsexlem9  28225  precsexlem11  28227  eucliddivs  28386  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  bdayfinbnd  28479  elz12s  28482  z12zsodd  28492  z12sge0  28493  remulscllem1  28510  istrkgld  28545  istrkg3ld  28547  axtgupdim2  28557  axtgeucl  28558  legov  28671  iscgra  28895  dfcgra2  28916  axsegconlem1  29004  axpasch  29028  axlowdim  29048  axeuclidlem  29049  nb3grpr  29469  upgr4cycl4dv4e  30273  vdgn1frgrv2  30384  fusgr2wsp2nb  30422  l2p  30568  br8d  32700  gsumwun  33157  constrsuc  33922  constrsslem  33925  constrconj  33929  constrllcllem  33936  constrlccllem  33937  constrcccllem  33938  constrcbvlem  33939  pstmval  34079  eulerpartlemgh  34562  eulerpartlemgs2  34564  cvmliftlem15  35526  cvmlift2lem10  35540  satf  35581  satfv0  35586  satfrnmapom  35598  satfv0fun  35599  satf0op  35605  sat1el2xp  35607  fmlafvel  35613  fmla1  35615  fmlaomn0  35618  gonan0  35620  goaln0  35621  gonar  35623  goalr  35625  fmlasucdisj  35627  satffunlem2lem1  35632  dmopab3rexdif  35633  satfv0fvfmla0  35641  sategoelfvb  35647  satfv1fvfmla1  35651  2goelgoanfmla1  35652  br8  35984  br6  35985  br4  35986  elaltxp  36203  brsegle  36336  ellines  36380  nn0prpwlem  36550  nn0prpw  36551  ptrest  37986  ismblfin  38028  itg2addnclem3  38040  itg2addnc  38041  releldmqscoss  39112  isline  40231  psubspi  40239  paddfval  40289  elpadd  40291  paddvaln0N  40293  3rspcedvd  42703  flt4lem7  43109  nna4b4nsq  43110  mzpcompact2lem  43200  mzpcompact2  43201  pell1qrval  43291  elpell1qr  43292  pell14qrval  43293  elpell14qr  43294  pell1234qrval  43295  elpell1234qr  43296  jm2.27  43453  expdiophlem1  43466  oenord1  43761  oaun3lem1  43819  clsk1independent  44490  limclner  46094  fourierdlem42  46592  fourierdlem48  46597  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