Theorem 2rexbidv 3209

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-rex 3060

This theorem is referenced by:  f1oiso  7353  elrnmpog  7550  elrnmpo  7551  ralrnmpo  7554  ovelrn  7591  opiota  8066  omeu  8605  oeeui  8622  eroveu  8834  erov  8836  elfiun  9452  dffi3  9453  xpwdomg  9607  brdom7disj  10553  brdom6disj  10554  genpv  11021  genpelv  11022  axcnre  11186  supadd  12218  supmullem1  12220  supmullem2  12221  supmul  12222  01sqrexlem6  15269  ello1  15534  ello1mpt  15540  elo1  15545  lo1o1  15551  o1lo1  15556  bezoutlem1  16559  bezoutlem3  16561  bezoutlem4  16562  bezout  16563  pythagtriplem2  16838  pythagtriplem19  16854  pythagtrip  16855  pcval  16865  pceu  16867  pczpre  16868  pcdiv  16873  4sqlem2  16970  4sqlem3  16971  4sqlem4  16973  4sq  16985  vdwlem1  17002  vdwlem12  17013  vdwlem13  17014  vdwnnlem1  17016  vdwnnlem2  17017  vdwnnlem3  17018  vdwnn  17019  ramub2  17035  rami  17036  cat1lem  18113  cat1  18114  pgpfac1lem3  20066  lspprel  21062  znunit  21537  cayleyhamiltonALT  22846  hausnei  23283  isreg2  23332  txuni2  23520  txbas  23522  xkoopn  23544  txcls  23559  txcnpi  23563  txdis1cn  23590  txtube  23595  txcmplem1  23596  hausdiag  23600  tx1stc  23605  regr1lem2  23695  qustgplem  24076  met2ndci  24480  dyadmax  25570  i1fadd  25667  i1fmul  25668  elply  26171  2sqlem2  27399  2sqlem8  27407  2sqlem9  27408  2sqlem11  27410  elmade  27843  mulsval  28072  mulsval2lem  28073  mulsproplem9  28087  mulsproplem12  28090  ssltmul1  28110  ssltmul2  28111  mulsuniflem  28112  addsdilem2  28115  mulsasslem1  28126  mulsasslem2  28127  mulsunif2  28133  precsexlemcbv  28167  precsexlem9  28176  precsexlem11  28178  elzs12  28358  remulscllem1  28369  istrkgld  28404  istrkg3ld  28406  axtgupdim2  28416  axtgeucl  28417  legov  28530  iscgra  28754  dfcgra2  28775  axsegconlem1  28863  axpasch  28887  axlowdim  28907  axeuclidlem  28908  nb3grpr  29328  upgr4cycl4dv4e  30133  vdgn1frgrv2  30244  fusgr2wsp2nb  30282  l2p  30427  br8d  32558  gsumwun  33012  constrsuc  33723  constrsslem  33726  constrconj  33730  constrllcllem  33737  constrlccllem  33738  constrcccllem  33739  constrcbvlem  33740  pstmval  33869  eulerpartlemgh  34355  eulerpartlemgs2  34357  cvmliftlem15  35278  cvmlift2lem10  35292  satf  35333  satfv0  35338  satfrnmapom  35350  satfv0fun  35351  satf0op  35357  sat1el2xp  35359  fmlafvel  35365  fmla1  35367  fmlaomn0  35370  gonan0  35372  goaln0  35373  gonar  35375  goalr  35377  fmlasucdisj  35379  satffunlem2lem1  35384  dmopab3rexdif  35385  satfv0fvfmla0  35393  sategoelfvb  35399  satfv1fvfmla1  35403  2goelgoanfmla1  35404  br8  35731  br6  35732  br4  35733  elaltxp  35951  brsegle  36084  ellines  36128  nn0prpwlem  36298  nn0prpw  36299  ptrest  37601  ismblfin  37643  itg2addnclem3  37655  itg2addnc  37656  releldmqscoss  38636  isline  39716  psubspi  39724  paddfval  39774  elpadd  39776  paddvaln0N  39778  3rspcedvd  42229  flt4lem7  42648  nna4b4nsq  42649  mzpcompact2lem  42740  mzpcompact2  42741  sbc4rexgOLD  42779  pell1qrval  42835  elpell1qr  42836  pell14qrval  42837  elpell14qr  42838  pell1234qrval  42839  elpell1234qr  42840  jm2.27  42998  expdiophlem1  43011  oenord1  43306  oaun3lem1  43364  clsk1independent  44036  limclner  45638  fourierdlem42  46136  fourierdlem48  46141  sprel  47444  prelspr  47446  prprelb  47476  prprelprb  47477  reuprpr  47483  isgbe  47711  isgbow  47712  isgbo  47713  sbgoldbalt  47741  sgoldbeven3prm  47743  mogoldbb  47745  sbgoldbo  47747  nnsum3primesle9  47754  usgrgrtrirex  47890  grlimgrtri  47936  bigoval  48443  elbigo  48445  iscnrm3r  48829  iscnrm3l  48832