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

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

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3070

This theorem is referenced by:  f1oiso  7301  elrnmpog  7496  elrnmpo  7497  ralrnmpo  7499  ovelrn  7535  opiota  7996  omeu  8537  oeeui  8554  eroveu  8758  erov  8760  elfiun  9375  dffi3  9376  xpwdomg  9530  brdom7disj  10476  brdom6disj  10477  genpv  10944  genpelv  10945  axcnre  11109  supadd  12132  supmullem1  12134  supmullem2  12135  supmul  12136  01sqrexlem6  15144  ello1  15409  ello1mpt  15415  elo1  15420  lo1o1  15426  o1lo1  15431  bezoutlem1  16431  bezoutlem3  16433  bezoutlem4  16434  bezout  16435  pythagtriplem2  16700  pythagtriplem19  16716  pythagtrip  16717  pcval  16727  pceu  16729  pczpre  16730  pcdiv  16735  4sqlem2  16832  4sqlem3  16833  4sqlem4  16835  4sq  16847  vdwlem1  16864  vdwlem12  16875  vdwlem13  16876  vdwnnlem1  16878  vdwnnlem2  16879  vdwnnlem3  16880  vdwnn  16881  ramub2  16897  rami  16898  cat1lem  17996  cat1  17997  pgpfac1lem3  19870  lspprel  20612  znunit  21007  cayleyhamiltonALT  22277  hausnei  22716  isreg2  22765  txuni2  22953  txbas  22955  xkoopn  22977  txcls  22992  txcnpi  22996  txdis1cn  23023  txtube  23028  txcmplem1  23029  hausdiag  23033  tx1stc  23038  regr1lem2  23128  qustgplem  23509  met2ndci  23915  dyadmax  24999  i1fadd  25096  i1fmul  25097  elply  25593  2sqlem2  26803  2sqlem8  26811  2sqlem9  26812  2sqlem11  26814  elmade  27240  mulsval  27417  mulsproplem10  27431  istrkgld  27464  istrkg3ld  27466  axtgupdim2  27476  axtgeucl  27477  legov  27590  iscgra  27814  dfcgra2  27835  axsegconlem1  27929  axpasch  27953  axlowdim  27973  axeuclidlem  27974  nb3grpr  28393  upgr4cycl4dv4e  29192  vdgn1frgrv2  29303  fusgr2wsp2nb  29341  l2p  29484  br8d  31596  pstmval  32565  eulerpartlemgh  33067  eulerpartlemgs2  33069  cvmliftlem15  33979  cvmlift2lem10  33993  satf  34034  satfv0  34039  satfrnmapom  34051  satfv0fun  34052  satf0op  34058  sat1el2xp  34060  fmlafvel  34066  fmla1  34068  fmlaomn0  34071  gonan0  34073  goaln0  34074  gonar  34076  goalr  34078  fmlasucdisj  34080  satffunlem2lem1  34085  dmopab3rexdif  34086  satfv0fvfmla0  34094  sategoelfvb  34100  satfv1fvfmla1  34104  2goelgoanfmla1  34105  br8  34415  br6  34416  br4  34417  elaltxp  34636  brsegle  34769  ellines  34813  nn0prpwlem  34870  nn0prpw  34871  ptrest  36150  ismblfin  36192  itg2addnclem3  36204  itg2addnc  36205  releldmqscoss  37195  isline  38275  psubspi  38283  paddfval  38333  elpadd  38335  paddvaln0N  38337  3rspcedvd  40707  flt4lem7  41055  nna4b4nsq  41056  mzpcompact2lem  41132  mzpcompact2  41133  sbc4rexgOLD  41171  pell1qrval  41227  elpell1qr  41228  pell14qrval  41229  elpell14qr  41230  pell1234qrval  41231  elpell1234qr  41232  jm2.27  41390  expdiophlem1  41403  oenord1  41709  oaun3lem1  41767  clsk1independent  42440  limclner  44012  fourierdlem42  44510  fourierdlem48  44515  sprel  45796  prelspr  45798  prprelb  45828  prprelprb  45829  reuprpr  45835  isgbe  46063  isgbow  46064  isgbo  46065  sbgoldbalt  46093  sgoldbeven3prm  46095  mogoldbb  46097  sbgoldbo  46099  nnsum3primesle9  46106  bigoval  46755  elbigo  46757  iscnrm3r  47101  iscnrm3l  47104