Theorem 2rexbidv 3219

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  f1oiso  7370  elrnmpog  7567  elrnmpo  7568  ralrnmpo  7571  ovelrn  7608  opiota  8082  omeu  8621  oeeui  8638  eroveu  8850  erov  8852  elfiun  9467  dffi3  9468  xpwdomg  9622  brdom7disj  10568  brdom6disj  10569  genpv  11036  genpelv  11037  axcnre  11201  supadd  12233  supmullem1  12235  supmullem2  12236  supmul  12237  01sqrexlem6  15282  ello1  15547  ello1mpt  15553  elo1  15558  lo1o1  15564  o1lo1  15569  bezoutlem1  16572  bezoutlem3  16574  bezoutlem4  16575  bezout  16576  pythagtriplem2  16850  pythagtriplem19  16866  pythagtrip  16867  pcval  16877  pceu  16879  pczpre  16880  pcdiv  16885  4sqlem2  16982  4sqlem3  16983  4sqlem4  16985  4sq  16997  vdwlem1  17014  vdwlem12  17025  vdwlem13  17026  vdwnnlem1  17028  vdwnnlem2  17029  vdwnnlem3  17030  vdwnn  17031  ramub2  17047  rami  17048  cat1lem  18149  cat1  18150  pgpfac1lem3  20111  lspprel  21110  znunit  21599  cayleyhamiltonALT  22912  hausnei  23351  isreg2  23400  txuni2  23588  txbas  23590  xkoopn  23612  txcls  23627  txcnpi  23631  txdis1cn  23658  txtube  23663  txcmplem1  23664  hausdiag  23668  tx1stc  23673  regr1lem2  23763  qustgplem  24144  met2ndci  24550  dyadmax  25646  i1fadd  25743  i1fmul  25744  elply  26248  2sqlem2  27476  2sqlem8  27484  2sqlem9  27485  2sqlem11  27487  elmade  27920  mulsval  28149  mulsval2lem  28150  mulsproplem9  28164  mulsproplem12  28167  ssltmul1  28187  ssltmul2  28188  mulsuniflem  28189  addsdilem2  28192  mulsasslem1  28203  mulsasslem2  28204  mulsunif2  28210  precsexlemcbv  28244  precsexlem9  28253  precsexlem11  28255  elzs12  28435  remulscllem1  28446  istrkgld  28481  istrkg3ld  28483  axtgupdim2  28493  axtgeucl  28494  legov  28607  iscgra  28831  dfcgra2  28852  axsegconlem1  28946  axpasch  28970  axlowdim  28990  axeuclidlem  28991  nb3grpr  29413  upgr4cycl4dv4e  30213  vdgn1frgrv2  30324  fusgr2wsp2nb  30362  l2p  30507  br8d  32629  gsumwun  33050  constrsuc  33742  constrsslem  33745  constrconj  33749  pstmval  33855  eulerpartlemgh  34359  eulerpartlemgs2  34361  cvmliftlem15  35282  cvmlift2lem10  35296  satf  35337  satfv0  35342  satfrnmapom  35354  satfv0fun  35355  satf0op  35361  sat1el2xp  35363  fmlafvel  35369  fmla1  35371  fmlaomn0  35374  gonan0  35376  goaln0  35377  gonar  35379  goalr  35381  fmlasucdisj  35383  satffunlem2lem1  35388  dmopab3rexdif  35389  satfv0fvfmla0  35397  sategoelfvb  35403  satfv1fvfmla1  35407  2goelgoanfmla1  35408  br8  35735  br6  35736  br4  35737  elaltxp  35956  brsegle  36089  ellines  36133  nn0prpwlem  36304  nn0prpw  36305  ptrest  37605  ismblfin  37647  itg2addnclem3  37659  itg2addnc  37660  releldmqscoss  38641  isline  39721  psubspi  39729  paddfval  39779  elpadd  39781  paddvaln0N  39783  3rspcedvd  42232  flt4lem7  42645  nna4b4nsq  42646  mzpcompact2lem  42738  mzpcompact2  42739  sbc4rexgOLD  42777  pell1qrval  42833  elpell1qr  42834  pell14qrval  42835  elpell14qr  42836  pell1234qrval  42837  elpell1234qr  42838  jm2.27  42996  expdiophlem1  43009  oenord1  43305  oaun3lem1  43363  clsk1independent  44035  limclner  45606  fourierdlem42  46104  fourierdlem48  46109  sprel  47408  prelspr  47410  prprelb  47440  prprelprb  47441  reuprpr  47447  isgbe  47675  isgbow  47676  isgbo  47677  sbgoldbalt  47705  sgoldbeven3prm  47707  mogoldbb  47709  sbgoldbo  47711  nnsum3primesle9  47718  usgrgrtrirex  47852  grlimgrtri  47898  bigoval  48398  elbigo  48400  iscnrm3r  48744  iscnrm3l  48747