Theorem 2rexbidv 3200

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

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

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 3054

This theorem is referenced by:  f1oiso  7308  elrnmpog  7504  elrnmpo  7505  ralrnmpo  7508  ovelrn  7545  opiota  8017  omeu  8526  oeeui  8543  eroveu  8762  erov  8764  elfiun  9357  dffi3  9358  xpwdomg  9514  brdom7disj  10460  brdom6disj  10461  genpv  10928  genpelv  10929  axcnre  11093  supadd  12127  supmullem1  12129  supmullem2  12130  supmul  12131  01sqrexlem6  15189  ello1  15457  ello1mpt  15463  elo1  15468  lo1o1  15474  o1lo1  15479  bezoutlem1  16485  bezoutlem3  16487  bezoutlem4  16488  bezout  16489  pythagtriplem2  16764  pythagtriplem19  16780  pythagtrip  16781  pcval  16791  pceu  16793  pczpre  16794  pcdiv  16799  4sqlem2  16896  4sqlem3  16897  4sqlem4  16899  4sq  16911  vdwlem1  16928  vdwlem12  16939  vdwlem13  16940  vdwnnlem1  16942  vdwnnlem2  16943  vdwnnlem3  16944  vdwnn  16945  ramub2  16961  rami  16962  cat1lem  18034  cat1  18035  pgpfac1lem3  19985  lspprel  20977  znunit  21449  cayleyhamiltonALT  22754  hausnei  23191  isreg2  23240  txuni2  23428  txbas  23430  xkoopn  23452  txcls  23467  txcnpi  23471  txdis1cn  23498  txtube  23503  txcmplem1  23504  hausdiag  23508  tx1stc  23513  regr1lem2  23603  qustgplem  23984  met2ndci  24386  dyadmax  25475  i1fadd  25572  i1fmul  25573  elply  26076  2sqlem2  27305  2sqlem8  27313  2sqlem9  27314  2sqlem11  27316  elmade  27755  mulsval  27988  mulsval2lem  27989  mulsproplem9  28003  mulsproplem12  28006  ssltmul1  28026  ssltmul2  28027  mulsuniflem  28028  addsdilem2  28031  mulsasslem1  28042  mulsasslem2  28043  mulsunif2  28049  precsexlemcbv  28084  precsexlem9  28093  precsexlem11  28095  eucliddivs  28241  elzs12  28313  zs12ge0  28318  remulscllem1  28327  istrkgld  28362  istrkg3ld  28364  axtgupdim2  28374  axtgeucl  28375  legov  28488  iscgra  28712  dfcgra2  28733  axsegconlem1  28820  axpasch  28844  axlowdim  28864  axeuclidlem  28865  nb3grpr  29285  upgr4cycl4dv4e  30087  vdgn1frgrv2  30198  fusgr2wsp2nb  30236  l2p  30381  br8d  32511  gsumwun  32978  constrsuc  33701  constrsslem  33704  constrconj  33708  constrllcllem  33715  constrlccllem  33716  constrcccllem  33717  constrcbvlem  33718  pstmval  33858  eulerpartlemgh  34342  eulerpartlemgs2  34344  cvmliftlem15  35258  cvmlift2lem10  35272  satf  35313  satfv0  35318  satfrnmapom  35330  satfv0fun  35331  satf0op  35337  sat1el2xp  35339  fmlafvel  35345  fmla1  35347  fmlaomn0  35350  gonan0  35352  goaln0  35353  gonar  35355  goalr  35357  fmlasucdisj  35359  satffunlem2lem1  35364  dmopab3rexdif  35365  satfv0fvfmla0  35373  sategoelfvb  35379  satfv1fvfmla1  35383  2goelgoanfmla1  35384  br8  35716  br6  35717  br4  35718  elaltxp  35936  brsegle  36069  ellines  36113  nn0prpwlem  36283  nn0prpw  36284  ptrest  37586  ismblfin  37628  itg2addnclem3  37640  itg2addnc  37641  releldmqscoss  38625  isline  39706  psubspi  39714  paddfval  39764  elpadd  39766  paddvaln0N  39768  3rspcedvd  42176  flt4lem7  42620  nna4b4nsq  42621  mzpcompact2lem  42712  mzpcompact2  42713  sbc4rexgOLD  42751  pell1qrval  42807  elpell1qr  42808  pell14qrval  42809  elpell14qr  42810  pell1234qrval  42811  elpell1234qr  42812  jm2.27  42970  expdiophlem1  42983  oenord1  43278  oaun3lem1  43336  clsk1independent  44008  limclner  45622  fourierdlem42  46120  fourierdlem48  46125  sprel  47458  prelspr  47460  prprelb  47490  prprelprb  47491  reuprpr  47497  isgbe  47725  isgbow  47726  isgbo  47727  sbgoldbalt  47755  sgoldbeven3prm  47757  mogoldbb  47759  sbgoldbo  47761  nnsum3primesle9  47768  usgrgrtrirex  47922  grlimgrtri  47968  bigoval  48511  elbigo  48513  iscnrm3r  48909  iscnrm3l  48912