Theorem 2rexbidv 3202

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

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

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 3062

This theorem is referenced by:  f1oiso  7306  elrnmpog  7502  elrnmpo  7503  ralrnmpo  7506  ovelrn  7543  opiota  8012  omeu  8520  oeeui  8538  eroveu  8759  erov  8761  elfiun  9343  dffi3  9344  xpwdomg  9500  brdom7disj  10453  brdom6disj  10454  genpv  10922  genpelv  10923  axcnre  11087  supadd  12124  supmullem1  12126  supmullem2  12127  supmul  12128  01sqrexlem6  15209  ello1  15477  ello1mpt  15483  elo1  15488  lo1o1  15494  o1lo1  15499  bezoutlem1  16508  bezoutlem3  16510  bezoutlem4  16511  bezout  16512  pythagtriplem2  16788  pythagtriplem19  16804  pythagtrip  16805  pcval  16815  pceu  16817  pczpre  16818  pcdiv  16823  4sqlem2  16920  4sqlem3  16921  4sqlem4  16923  4sq  16935  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  vdwnnlem1  16966  vdwnnlem2  16967  vdwnnlem3  16968  vdwnn  16969  ramub2  16985  rami  16986  cat1lem  18063  cat1  18064  pgpfac1lem3  20054  lspprel  21089  znunit  21543  cayleyhamiltonALT  22856  hausnei  23293  isreg2  23342  txuni2  23530  txbas  23532  xkoopn  23554  txcls  23569  txcnpi  23573  txdis1cn  23600  txtube  23605  txcmplem1  23606  hausdiag  23610  tx1stc  23615  regr1lem2  23705  qustgplem  24086  met2ndci  24487  dyadmax  25565  i1fadd  25662  i1fmul  25663  elply  26160  2sqlem2  27381  2sqlem8  27389  2sqlem9  27390  2sqlem11  27392  elmade  27849  mulsval  28101  mulsval2lem  28102  mulsproplem9  28116  mulsproplem12  28119  sltmuls1  28139  sltmuls2  28140  mulsuniflem  28141  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  mulsunif2  28162  precsexlemcbv  28198  precsexlem9  28207  precsexlem11  28209  eucliddivs  28368  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  bdayfinbnd  28461  elz12s  28464  z12zsodd  28474  z12sge0  28475  remulscllem1  28492  istrkgld  28527  istrkg3ld  28529  axtgupdim2  28539  axtgeucl  28540  legov  28653  iscgra  28877  dfcgra2  28898  axsegconlem1  28986  axpasch  29010  axlowdim  29030  axeuclidlem  29031  nb3grpr  29451  upgr4cycl4dv4e  30255  vdgn1frgrv2  30366  fusgr2wsp2nb  30404  l2p  30550  br8d  32681  gsumwun  33137  constrsuc  33882  constrsslem  33885  constrconj  33889  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  constrcbvlem  33899  pstmval  34039  eulerpartlemgh  34522  eulerpartlemgs2  34524  cvmliftlem15  35480  cvmlift2lem10  35494  satf  35535  satfv0  35540  satfrnmapom  35552  satfv0fun  35553  satf0op  35559  sat1el2xp  35561  fmlafvel  35567  fmla1  35569  fmlaomn0  35572  gonan0  35574  goaln0  35575  gonar  35577  goalr  35579  fmlasucdisj  35581  satffunlem2lem1  35586  dmopab3rexdif  35587  satfv0fvfmla0  35595  sategoelfvb  35601  satfv1fvfmla1  35605  2goelgoanfmla1  35606  br8  35938  br6  35939  br4  35940  elaltxp  36157  brsegle  36290  ellines  36334  nn0prpwlem  36504  nn0prpw  36505  ptrest  37940  ismblfin  37982  itg2addnclem3  37994  itg2addnc  37995  releldmqscoss  39066  isline  40185  psubspi  40193  paddfval  40243  elpadd  40245  paddvaln0N  40247  3rspcedvd  42657  flt4lem7  43092  nna4b4nsq  43093  mzpcompact2lem  43183  mzpcompact2  43184  pell1qrval  43274  elpell1qr  43275  pell14qrval  43276  elpell14qr  43277  pell1234qrval  43278  elpell1234qr  43279  jm2.27  43436  expdiophlem1  43449  oenord1  43744  oaun3lem1  43802  clsk1independent  44473  limclner  46079  fourierdlem42  46577  fourierdlem48  46582  sprel  47944  prelspr  47946  prprelb  47976  prprelprb  47977  reuprpr  47983  isgbe  48227  isgbow  48228  isgbo  48229  sbgoldbalt  48257  sgoldbeven3prm  48259  mogoldbb  48261  sbgoldbo  48263  nnsum3primesle9  48270  usgrgrtrirex  48426  grlimgrtri  48479  grlimedgnedg  48607  bigoval  49025  elbigo  49027  iscnrm3r  49423  iscnrm3l  49426