Theorem 2rexbidv 3202

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  7326  elrnmpog  7524  elrnmpo  7525  ralrnmpo  7528  ovelrn  7565  opiota  8038  omeu  8549  oeeui  8566  eroveu  8785  erov  8787  elfiun  9381  dffi3  9382  xpwdomg  9538  brdom7disj  10484  brdom6disj  10485  genpv  10952  genpelv  10953  axcnre  11117  supadd  12151  supmullem1  12153  supmullem2  12154  supmul  12155  01sqrexlem6  15213  ello1  15481  ello1mpt  15487  elo1  15492  lo1o1  15498  o1lo1  15503  bezoutlem1  16509  bezoutlem3  16511  bezoutlem4  16512  bezout  16513  pythagtriplem2  16788  pythagtriplem19  16804  pythagtrip  16805  pcval  16815  pceu  16817  pczpre  16818  pcdiv  16823  4sqlem2  16920  4sqlem3  16921  4sqlem4  16923  4sq  16935  vdwlem1  16952  vdwlem12  16963  vdwlem13  16964  vdwnnlem1  16966  vdwnnlem2  16967  vdwnnlem3  16968  vdwnn  16969  ramub2  16985  rami  16986  cat1lem  18058  cat1  18059  pgpfac1lem3  20009  lspprel  21001  znunit  21473  cayleyhamiltonALT  22778  hausnei  23215  isreg2  23264  txuni2  23452  txbas  23454  xkoopn  23476  txcls  23491  txcnpi  23495  txdis1cn  23522  txtube  23527  txcmplem1  23528  hausdiag  23532  tx1stc  23537  regr1lem2  23627  qustgplem  24008  met2ndci  24410  dyadmax  25499  i1fadd  25596  i1fmul  25597  elply  26100  2sqlem2  27329  2sqlem8  27337  2sqlem9  27338  2sqlem11  27340  elmade  27779  mulsval  28012  mulsval2lem  28013  mulsproplem9  28027  mulsproplem12  28030  ssltmul1  28050  ssltmul2  28051  mulsuniflem  28052  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  mulsunif2  28073  precsexlemcbv  28108  precsexlem9  28117  precsexlem11  28119  eucliddivs  28265  elzs12  28337  zs12ge0  28342  remulscllem1  28351  istrkgld  28386  istrkg3ld  28388  axtgupdim2  28398  axtgeucl  28399  legov  28512  iscgra  28736  dfcgra2  28757  axsegconlem1  28844  axpasch  28868  axlowdim  28888  axeuclidlem  28889  nb3grpr  29309  upgr4cycl4dv4e  30114  vdgn1frgrv2  30225  fusgr2wsp2nb  30263  l2p  30408  br8d  32538  gsumwun  33005  constrsuc  33728  constrsslem  33731  constrconj  33735  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  constrcbvlem  33745  pstmval  33885  eulerpartlemgh  34369  eulerpartlemgs2  34371  cvmliftlem15  35285  cvmlift2lem10  35299  satf  35340  satfv0  35345  satfrnmapom  35357  satfv0fun  35358  satf0op  35364  sat1el2xp  35366  fmlafvel  35372  fmla1  35374  fmlaomn0  35377  gonan0  35379  goaln0  35380  gonar  35382  goalr  35384  fmlasucdisj  35386  satffunlem2lem1  35391  dmopab3rexdif  35392  satfv0fvfmla0  35400  sategoelfvb  35406  satfv1fvfmla1  35410  2goelgoanfmla1  35411  br8  35743  br6  35744  br4  35745  elaltxp  35963  brsegle  36096  ellines  36140  nn0prpwlem  36310  nn0prpw  36311  ptrest  37613  ismblfin  37655  itg2addnclem3  37667  itg2addnc  37668  releldmqscoss  38652  isline  39733  psubspi  39741  paddfval  39791  elpadd  39793  paddvaln0N  39795  3rspcedvd  42203  flt4lem7  42647  nna4b4nsq  42648  mzpcompact2lem  42739  mzpcompact2  42740  sbc4rexgOLD  42778  pell1qrval  42834  elpell1qr  42835  pell14qrval  42836  elpell14qr  42837  pell1234qrval  42838  elpell1234qr  42839  jm2.27  42997  expdiophlem1  43010  oenord1  43305  oaun3lem1  43363  clsk1independent  44035  limclner  45649  fourierdlem42  46147  fourierdlem48  46152  sprel  47485  prelspr  47487  prprelb  47517  prprelprb  47518  reuprpr  47524  isgbe  47752  isgbow  47753  isgbo  47754  sbgoldbalt  47782  sgoldbeven3prm  47784  mogoldbb  47786  sbgoldbo  47788  nnsum3primesle9  47795  usgrgrtrirex  47949  grlimgrtri  47995  bigoval  48538  elbigo  48540  iscnrm3r  48936  iscnrm3l  48939