Theorem 2rexbidv 3220

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

Syntax hints:   → wi 4   ↔ wb 205  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  f1oiso  7348  elrnmpog  7544  elrnmpo  7545  ralrnmpo  7547  ovelrn  7583  opiota  8045  omeu  8585  oeeui  8602  eroveu  8806  erov  8808  elfiun  9425  dffi3  9426  xpwdomg  9580  brdom7disj  10526  brdom6disj  10527  genpv  10994  genpelv  10995  axcnre  11159  supadd  12182  supmullem1  12184  supmullem2  12185  supmul  12186  01sqrexlem6  15194  ello1  15459  ello1mpt  15465  elo1  15470  lo1o1  15476  o1lo1  15481  bezoutlem1  16481  bezoutlem3  16483  bezoutlem4  16484  bezout  16485  pythagtriplem2  16750  pythagtriplem19  16766  pythagtrip  16767  pcval  16777  pceu  16779  pczpre  16780  pcdiv  16785  4sqlem2  16882  4sqlem3  16883  4sqlem4  16885  4sq  16897  vdwlem1  16914  vdwlem12  16925  vdwlem13  16926  vdwnnlem1  16928  vdwnnlem2  16929  vdwnnlem3  16930  vdwnn  16931  ramub2  16947  rami  16948  cat1lem  18046  cat1  18047  pgpfac1lem3  19947  lspprel  20705  znunit  21119  cayleyhamiltonALT  22393  hausnei  22832  isreg2  22881  txuni2  23069  txbas  23071  xkoopn  23093  txcls  23108  txcnpi  23112  txdis1cn  23139  txtube  23144  txcmplem1  23145  hausdiag  23149  tx1stc  23154  regr1lem2  23244  qustgplem  23625  met2ndci  24031  dyadmax  25115  i1fadd  25212  i1fmul  25213  elply  25709  2sqlem2  26921  2sqlem8  26929  2sqlem9  26930  2sqlem11  26932  elmade  27362  mulsval  27565  mulsval2lem  27566  mulsproplem9  27580  mulsproplem12  27583  ssltmul1  27602  ssltmul2  27603  mulsuniflem  27604  addsdilem2  27607  mulsasslem1  27618  mulsasslem2  27619  precsexlemcbv  27652  precsexlem9  27661  precsexlem11  27663  istrkgld  27710  istrkg3ld  27712  axtgupdim2  27722  axtgeucl  27723  legov  27836  iscgra  28060  dfcgra2  28081  axsegconlem1  28175  axpasch  28199  axlowdim  28219  axeuclidlem  28220  nb3grpr  28639  upgr4cycl4dv4e  29438  vdgn1frgrv2  29549  fusgr2wsp2nb  29587  l2p  29732  br8d  31839  pstmval  32875  eulerpartlemgh  33377  eulerpartlemgs2  33379  cvmliftlem15  34289  cvmlift2lem10  34303  satf  34344  satfv0  34349  satfrnmapom  34361  satfv0fun  34362  satf0op  34368  sat1el2xp  34370  fmlafvel  34376  fmla1  34378  fmlaomn0  34381  gonan0  34383  goaln0  34384  gonar  34386  goalr  34388  fmlasucdisj  34390  satffunlem2lem1  34395  dmopab3rexdif  34396  satfv0fvfmla0  34404  sategoelfvb  34410  satfv1fvfmla1  34414  2goelgoanfmla1  34415  br8  34726  br6  34727  br4  34728  elaltxp  34947  brsegle  35080  ellines  35124  nn0prpwlem  35207  nn0prpw  35208  ptrest  36487  ismblfin  36529  itg2addnclem3  36541  itg2addnc  36542  releldmqscoss  37530  isline  38610  psubspi  38618  paddfval  38668  elpadd  38670  paddvaln0N  38672  3rspcedvd  41031  flt4lem7  41401  nna4b4nsq  41402  mzpcompact2lem  41489  mzpcompact2  41490  sbc4rexgOLD  41528  pell1qrval  41584  elpell1qr  41585  pell14qrval  41586  elpell14qr  41587  pell1234qrval  41588  elpell1234qr  41589  jm2.27  41747  expdiophlem1  41760  oenord1  42066  oaun3lem1  42124  clsk1independent  42797  limclner  44367  fourierdlem42  44865  fourierdlem48  44870  sprel  46152  prelspr  46154  prprelb  46184  prprelprb  46185  reuprpr  46191  isgbe  46419  isgbow  46420  isgbo  46421  sbgoldbalt  46449  sgoldbeven3prm  46451  mogoldbb  46453  sbgoldbo  46455  nnsum3primesle9  46462  bigoval  47235  elbigo  47237  iscnrm3r  47581  iscnrm3l  47584