Theorem 2rexbidv 3206

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

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

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 3061

This theorem is referenced by:  f1oiso  7344  elrnmpog  7542  elrnmpo  7543  ralrnmpo  7546  ovelrn  7583  opiota  8058  omeu  8597  oeeui  8614  eroveu  8826  erov  8828  elfiun  9442  dffi3  9443  xpwdomg  9599  brdom7disj  10545  brdom6disj  10546  genpv  11013  genpelv  11014  axcnre  11178  supadd  12210  supmullem1  12212  supmullem2  12213  supmul  12214  01sqrexlem6  15266  ello1  15531  ello1mpt  15537  elo1  15542  lo1o1  15548  o1lo1  15553  bezoutlem1  16558  bezoutlem3  16560  bezoutlem4  16561  bezout  16562  pythagtriplem2  16837  pythagtriplem19  16853  pythagtrip  16854  pcval  16864  pceu  16866  pczpre  16867  pcdiv  16872  4sqlem2  16969  4sqlem3  16970  4sqlem4  16972  4sq  16984  vdwlem1  17001  vdwlem12  17012  vdwlem13  17013  vdwnnlem1  17015  vdwnnlem2  17016  vdwnnlem3  17017  vdwnn  17018  ramub2  17034  rami  17035  cat1lem  18109  cat1  18110  pgpfac1lem3  20060  lspprel  21052  znunit  21524  cayleyhamiltonALT  22829  hausnei  23266  isreg2  23315  txuni2  23503  txbas  23505  xkoopn  23527  txcls  23542  txcnpi  23546  txdis1cn  23573  txtube  23578  txcmplem1  23579  hausdiag  23583  tx1stc  23588  regr1lem2  23678  qustgplem  24059  met2ndci  24461  dyadmax  25551  i1fadd  25648  i1fmul  25649  elply  26152  2sqlem2  27381  2sqlem8  27389  2sqlem9  27390  2sqlem11  27392  elmade  27831  mulsval  28064  mulsval2lem  28065  mulsproplem9  28079  mulsproplem12  28082  ssltmul1  28102  ssltmul2  28103  mulsuniflem  28104  addsdilem2  28107  mulsasslem1  28118  mulsasslem2  28119  mulsunif2  28125  precsexlemcbv  28160  precsexlem9  28169  precsexlem11  28171  eucliddivs  28317  elzs12  28389  zs12ge0  28394  remulscllem1  28403  istrkgld  28438  istrkg3ld  28440  axtgupdim2  28450  axtgeucl  28451  legov  28564  iscgra  28788  dfcgra2  28809  axsegconlem1  28896  axpasch  28920  axlowdim  28940  axeuclidlem  28941  nb3grpr  29361  upgr4cycl4dv4e  30166  vdgn1frgrv2  30277  fusgr2wsp2nb  30315  l2p  30460  br8d  32590  gsumwun  33059  constrsuc  33772  constrsslem  33775  constrconj  33779  constrllcllem  33786  constrlccllem  33787  constrcccllem  33788  constrcbvlem  33789  pstmval  33926  eulerpartlemgh  34410  eulerpartlemgs2  34412  cvmliftlem15  35320  cvmlift2lem10  35334  satf  35375  satfv0  35380  satfrnmapom  35392  satfv0fun  35393  satf0op  35399  sat1el2xp  35401  fmlafvel  35407  fmla1  35409  fmlaomn0  35412  gonan0  35414  goaln0  35415  gonar  35417  goalr  35419  fmlasucdisj  35421  satffunlem2lem1  35426  dmopab3rexdif  35427  satfv0fvfmla0  35435  sategoelfvb  35441  satfv1fvfmla1  35445  2goelgoanfmla1  35446  br8  35773  br6  35774  br4  35775  elaltxp  35993  brsegle  36126  ellines  36170  nn0prpwlem  36340  nn0prpw  36341  ptrest  37643  ismblfin  37685  itg2addnclem3  37697  itg2addnc  37698  releldmqscoss  38678  isline  39758  psubspi  39766  paddfval  39816  elpadd  39818  paddvaln0N  39820  3rspcedvd  42266  flt4lem7  42682  nna4b4nsq  42683  mzpcompact2lem  42774  mzpcompact2  42775  sbc4rexgOLD  42813  pell1qrval  42869  elpell1qr  42870  pell14qrval  42871  elpell14qr  42872  pell1234qrval  42873  elpell1234qr  42874  jm2.27  43032  expdiophlem1  43045  oenord1  43340  oaun3lem1  43398  clsk1independent  44070  limclner  45680  fourierdlem42  46178  fourierdlem48  46183  sprel  47498  prelspr  47500  prprelb  47530  prprelprb  47531  reuprpr  47537  isgbe  47765  isgbow  47766  isgbo  47767  sbgoldbalt  47795  sgoldbeven3prm  47797  mogoldbb  47799  sbgoldbo  47801  nnsum3primesle9  47808  usgrgrtrirex  47962  grlimgrtri  48008  bigoval  48529  elbigo  48531  iscnrm3r  48922  iscnrm3l  48925