Theorem 2rexbidv 3197

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  f1oiso  7285  elrnmpog  7481  elrnmpo  7482  ralrnmpo  7485  ovelrn  7522  opiota  7991  omeu  8500  oeeui  8517  eroveu  8736  erov  8738  elfiun  9314  dffi3  9315  xpwdomg  9471  brdom7disj  10422  brdom6disj  10423  genpv  10890  genpelv  10891  axcnre  11055  supadd  12090  supmullem1  12092  supmullem2  12093  supmul  12094  01sqrexlem6  15154  ello1  15422  ello1mpt  15428  elo1  15433  lo1o1  15439  o1lo1  15444  bezoutlem1  16450  bezoutlem3  16452  bezoutlem4  16453  bezout  16454  pythagtriplem2  16729  pythagtriplem19  16745  pythagtrip  16746  pcval  16756  pceu  16758  pczpre  16759  pcdiv  16764  4sqlem2  16861  4sqlem3  16862  4sqlem4  16864  4sq  16876  vdwlem1  16893  vdwlem12  16904  vdwlem13  16905  vdwnnlem1  16907  vdwnnlem2  16908  vdwnnlem3  16909  vdwnn  16910  ramub2  16926  rami  16927  cat1lem  18003  cat1  18004  pgpfac1lem3  19991  lspprel  21028  znunit  21500  cayleyhamiltonALT  22806  hausnei  23243  isreg2  23292  txuni2  23480  txbas  23482  xkoopn  23504  txcls  23519  txcnpi  23523  txdis1cn  23550  txtube  23555  txcmplem1  23556  hausdiag  23560  tx1stc  23565  regr1lem2  23655  qustgplem  24036  met2ndci  24437  dyadmax  25526  i1fadd  25623  i1fmul  25624  elply  26127  2sqlem2  27356  2sqlem8  27364  2sqlem9  27365  2sqlem11  27367  elmade  27812  mulsval  28048  mulsval2lem  28049  mulsproplem9  28063  mulsproplem12  28066  ssltmul1  28086  ssltmul2  28087  mulsuniflem  28088  addsdilem2  28091  mulsasslem1  28102  mulsasslem2  28103  mulsunif2  28109  precsexlemcbv  28144  precsexlem9  28153  precsexlem11  28155  eucliddivs  28301  elzs12  28383  zs12zodd  28392  zs12ge0  28393  remulscllem1  28402  istrkgld  28437  istrkg3ld  28439  axtgupdim2  28449  axtgeucl  28450  legov  28563  iscgra  28787  dfcgra2  28808  axsegconlem1  28895  axpasch  28919  axlowdim  28939  axeuclidlem  28940  nb3grpr  29360  upgr4cycl4dv4e  30165  vdgn1frgrv2  30276  fusgr2wsp2nb  30314  l2p  30459  br8d  32591  gsumwun  33045  constrsuc  33751  constrsslem  33754  constrconj  33758  constrllcllem  33765  constrlccllem  33766  constrcccllem  33767  constrcbvlem  33768  pstmval  33908  eulerpartlemgh  34391  eulerpartlemgs2  34393  cvmliftlem15  35342  cvmlift2lem10  35356  satf  35397  satfv0  35402  satfrnmapom  35414  satfv0fun  35415  satf0op  35421  sat1el2xp  35423  fmlafvel  35429  fmla1  35431  fmlaomn0  35434  gonan0  35436  goaln0  35437  gonar  35439  goalr  35441  fmlasucdisj  35443  satffunlem2lem1  35448  dmopab3rexdif  35449  satfv0fvfmla0  35457  sategoelfvb  35463  satfv1fvfmla1  35467  2goelgoanfmla1  35468  br8  35800  br6  35801  br4  35802  elaltxp  36017  brsegle  36150  ellines  36194  nn0prpwlem  36364  nn0prpw  36365  ptrest  37667  ismblfin  37709  itg2addnclem3  37721  itg2addnc  37722  releldmqscoss  38706  isline  39786  psubspi  39794  paddfval  39844  elpadd  39846  paddvaln0N  39848  3rspcedvd  42256  flt4lem7  42700  nna4b4nsq  42701  mzpcompact2lem  42792  mzpcompact2  42793  sbc4rexgOLD  42831  pell1qrval  42887  elpell1qr  42888  pell14qrval  42889  elpell14qr  42890  pell1234qrval  42891  elpell1234qr  42892  jm2.27  43049  expdiophlem1  43062  oenord1  43357  oaun3lem1  43415  clsk1independent  44087  limclner  45697  fourierdlem42  46195  fourierdlem48  46200  sprel  47523  prelspr  47525  prprelb  47555  prprelprb  47556  reuprpr  47562  isgbe  47790  isgbow  47791  isgbo  47792  sbgoldbalt  47820  sgoldbeven3prm  47822  mogoldbb  47824  sbgoldbo  47826  nnsum3primesle9  47833  usgrgrtrirex  47989  grlimgrtri  48042  grlimedgnedg  48170  bigoval  48589  elbigo  48591  iscnrm3r  48987  iscnrm3l  48990