Theorem 2rexbidv 3222

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 206  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  f1oiso  7371  elrnmpog  7568  elrnmpo  7569  ralrnmpo  7572  ovelrn  7609  opiota  8084  omeu  8623  oeeui  8640  eroveu  8852  erov  8854  elfiun  9470  dffi3  9471  xpwdomg  9625  brdom7disj  10571  brdom6disj  10572  genpv  11039  genpelv  11040  axcnre  11204  supadd  12236  supmullem1  12238  supmullem2  12239  supmul  12240  01sqrexlem6  15286  ello1  15551  ello1mpt  15557  elo1  15562  lo1o1  15568  o1lo1  15573  bezoutlem1  16576  bezoutlem3  16578  bezoutlem4  16579  bezout  16580  pythagtriplem2  16855  pythagtriplem19  16871  pythagtrip  16872  pcval  16882  pceu  16884  pczpre  16885  pcdiv  16890  4sqlem2  16987  4sqlem3  16988  4sqlem4  16990  4sq  17002  vdwlem1  17019  vdwlem12  17030  vdwlem13  17031  vdwnnlem1  17033  vdwnnlem2  17034  vdwnnlem3  17035  vdwnn  17036  ramub2  17052  rami  17053  cat1lem  18141  cat1  18142  pgpfac1lem3  20097  lspprel  21093  znunit  21582  cayleyhamiltonALT  22897  hausnei  23336  isreg2  23385  txuni2  23573  txbas  23575  xkoopn  23597  txcls  23612  txcnpi  23616  txdis1cn  23643  txtube  23648  txcmplem1  23649  hausdiag  23653  tx1stc  23658  regr1lem2  23748  qustgplem  24129  met2ndci  24535  dyadmax  25633  i1fadd  25730  i1fmul  25731  elply  26234  2sqlem2  27462  2sqlem8  27470  2sqlem9  27471  2sqlem11  27473  elmade  27906  mulsval  28135  mulsval2lem  28136  mulsproplem9  28150  mulsproplem12  28153  ssltmul1  28173  ssltmul2  28174  mulsuniflem  28175  addsdilem2  28178  mulsasslem1  28189  mulsasslem2  28190  mulsunif2  28196  precsexlemcbv  28230  precsexlem9  28239  precsexlem11  28241  elzs12  28421  remulscllem1  28432  istrkgld  28467  istrkg3ld  28469  axtgupdim2  28479  axtgeucl  28480  legov  28593  iscgra  28817  dfcgra2  28838  axsegconlem1  28932  axpasch  28956  axlowdim  28976  axeuclidlem  28977  nb3grpr  29399  upgr4cycl4dv4e  30204  vdgn1frgrv2  30315  fusgr2wsp2nb  30353  l2p  30498  br8d  32622  gsumwun  33068  constrsuc  33779  constrsslem  33782  constrconj  33786  pstmval  33894  eulerpartlemgh  34380  eulerpartlemgs2  34382  cvmliftlem15  35303  cvmlift2lem10  35317  satf  35358  satfv0  35363  satfrnmapom  35375  satfv0fun  35376  satf0op  35382  sat1el2xp  35384  fmlafvel  35390  fmla1  35392  fmlaomn0  35395  gonan0  35397  goaln0  35398  gonar  35400  goalr  35402  fmlasucdisj  35404  satffunlem2lem1  35409  dmopab3rexdif  35410  satfv0fvfmla0  35418  sategoelfvb  35424  satfv1fvfmla1  35428  2goelgoanfmla1  35429  br8  35756  br6  35757  br4  35758  elaltxp  35976  brsegle  36109  ellines  36153  nn0prpwlem  36323  nn0prpw  36324  ptrest  37626  ismblfin  37668  itg2addnclem3  37680  itg2addnc  37681  releldmqscoss  38661  isline  39741  psubspi  39749  paddfval  39799  elpadd  39801  paddvaln0N  39803  3rspcedvd  42254  flt4lem7  42669  nna4b4nsq  42670  mzpcompact2lem  42762  mzpcompact2  42763  sbc4rexgOLD  42801  pell1qrval  42857  elpell1qr  42858  pell14qrval  42859  elpell14qr  42860  pell1234qrval  42861  elpell1234qr  42862  jm2.27  43020  expdiophlem1  43033  oenord1  43329  oaun3lem1  43387  clsk1independent  44059  limclner  45666  fourierdlem42  46164  fourierdlem48  46169  sprel  47471  prelspr  47473  prprelb  47503  prprelprb  47504  reuprpr  47510  isgbe  47738  isgbow  47739  isgbo  47740  sbgoldbalt  47768  sgoldbeven3prm  47770  mogoldbb  47772  sbgoldbo  47774  nnsum3primesle9  47781  usgrgrtrirex  47917  grlimgrtri  47963  bigoval  48470  elbigo  48472  iscnrm3r  48845  iscnrm3l  48848