Theorem 2rexbidv 3300

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	rexbidv 3297	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3297	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 208  ∃wrex 3139

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 209  df-an 399  df-ex 1781  df-rex 3144

This theorem is referenced by:  f1oiso  7104  elrnmpog  7286  elrnmpo  7287  ralrnmpo  7289  ovelrn  7324  opiota  7757  omeu  8211  oeeui  8228  eroveu  8392  erov  8394  elfiun  8894  dffi3  8895  xpwdomg  9049  brdom7disj  9953  brdom6disj  9954  genpv  10421  genpelv  10422  axcnre  10586  supadd  11609  supmullem1  11611  supmullem2  11612  supmul  11613  sqrlem6  14607  ello1  14872  ello1mpt  14878  elo1  14883  lo1o1  14889  o1lo1  14894  bezoutlem1  15887  bezoutlem3  15889  bezoutlem4  15890  bezout  15891  pythagtriplem2  16154  pythagtriplem19  16170  pythagtrip  16171  pcval  16181  pceu  16183  pczpre  16184  pcdiv  16189  4sqlem2  16285  4sqlem3  16286  4sqlem4  16288  4sq  16300  vdwlem1  16317  vdwlem12  16328  vdwlem13  16329  vdwnnlem1  16331  vdwnnlem2  16332  vdwnnlem3  16333  vdwnn  16334  ramub2  16350  rami  16351  pgpfac1lem3  19199  lspprel  19866  znunit  20710  cayleyhamiltonALT  21499  hausnei  21936  isreg2  21985  txuni2  22173  txbas  22175  xkoopn  22197  txcls  22212  txcnpi  22216  txdis1cn  22243  txtube  22248  txcmplem1  22249  hausdiag  22253  tx1stc  22258  regr1lem2  22348  qustgplem  22729  met2ndci  23132  dyadmax  24199  i1fadd  24296  i1fmul  24297  elply  24785  2sqlem2  25994  2sqlem8  26002  2sqlem9  26003  2sqlem11  26005  istrkgld  26245  istrkg3ld  26247  axtgupdim2  26257  axtgeucl  26258  legov  26371  iscgra  26595  dfcgra2  26616  axsegconlem1  26703  axpasch  26727  axlowdim  26747  axeuclidlem  26748  nb3grpr  27164  upgr4cycl4dv4e  27964  vdgn1frgrv2  28075  fusgr2wsp2nb  28113  l2p  28256  br8d  30361  pstmval  31135  eulerpartlemgh  31636  eulerpartlemgs2  31638  cvmliftlem15  32545  cvmlift2lem10  32559  satf  32600  satfv0  32605  satfrnmapom  32617  satfv0fun  32618  satf0op  32624  sat1el2xp  32626  fmlafvel  32632  fmla1  32634  fmlaomn0  32637  gonan0  32639  goaln0  32640  gonar  32642  goalr  32644  fmlasucdisj  32646  satffunlem2lem1  32651  dmopab3rexdif  32652  satfv0fvfmla0  32660  sategoelfvb  32666  satfv1fvfmla1  32670  2goelgoanfmla1  32671  br8  32992  br6  32993  br4  32994  elaltxp  33436  brsegle  33569  ellines  33613  nn0prpwlem  33670  nn0prpw  33671  ptrest  34906  ismblfin  34948  itg2addnclem3  34960  itg2addnc  34961  releldmqscoss  35909  isline  36890  psubspi  36898  paddfval  36948  elpadd  36950  paddvaln0N  36952  3rspcedvd  39125  mzpcompact2lem  39368  mzpcompact2  39369  sbc4rexgOLD  39407  pell1qrval  39463  elpell1qr  39464  pell14qrval  39465  elpell14qr  39466  pell1234qrval  39467  elpell1234qr  39468  jm2.27  39625  expdiophlem1  39638  clsk1independent  40416  limclner  41952  fourierdlem42  42454  fourierdlem48  42459  sprel  43666  prelspr  43668  prprelb  43698  prprelprb  43699  reuprpr  43705  isgbe  43936  isgbow  43937  isgbo  43938  sbgoldbalt  43966  sgoldbeven3prm  43968  mogoldbb  43970  sbgoldbo  43972  nnsum3primesle9  43979  bigoval  44629  elbigo  44631