Theorem 2rexbidv 3039

Description: Formula-building rule for restricted existential quantifiers (deduction rule). (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 3034	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3034	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 195  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902

This theorem is referenced by:  f1oiso  6501  elrnmpt2g  6670  elrnmpt2  6671  ralrnmpt2  6673  ovelrn  6708  opiota  7118  omeu  7552  oeeui  7569  eroveu  7729  erov  7731  elfiun  8219  dffi3  8220  xpwdomg  8373  brdom7disj  9234  brdom6disj  9235  genpv  9700  genpelv  9701  axcnre  9864  supadd  10868  supmullem1  10870  supmullem2  10871  supmul  10872  sqrlem6  13836  ello1  14094  ello1mpt  14100  elo1  14105  lo1o1  14111  o1lo1  14116  bezoutlem1  15094  bezoutlem3  15096  bezoutlem4  15097  bezout  15098  pythagtriplem2  15360  pythagtriplem19  15376  pythagtrip  15377  pcval  15387  pceu  15389  pczpre  15390  pcdiv  15395  4sqlem2  15491  4sqlem3  15492  4sqlem4  15494  4sq  15506  vdwlem1  15523  vdwlem12  15534  vdwlem13  15535  vdwnnlem1  15537  vdwnnlem2  15538  vdwnnlem3  15539  vdwnn  15540  ramub2  15556  rami  15557  pgpfac1lem3  18299  lspprel  18915  znunit  19731  cayleyhamiltonALT  20515  hausnei  20942  isreg2  20991  txuni2  21178  txbas  21180  xkoopn  21202  txcls  21217  txcnpi  21221  txdis1cn  21248  txtube  21253  txcmplem1  21254  hausdiag  21258  tx1stc  21263  regr1lem2  21353  qustgplem  21734  met2ndci  22137  dyadmax  23172  i1fadd  23268  i1fmul  23269  elply  23755  2sqlem2  24943  2sqlem8  24951  2sqlem9  24952  2sqlem11  24954  istrkgld  25158  axtgeucl  25171  legov  25280  iscgra  25501  dfcgra2  25521  axsegconlem1  25597  axpasch  25621  axlowdim  25641  axeuclidlem  25642  nb3grapr  25982  el2wlksoton  26405  el2spthsoton  26406  el2wlksotot  26409  2wot2wont  26413  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  usg2spot2nb  26592  br8d  28802  pstmval  29266  eulerpartlemgh  29767  eulerpartlemgs2  29769  cvmliftlem15  30534  cvmlift2lem10  30548  br8  30899  br6  30900  br4  30901  nofulllem5  31105  elaltxp  31252  brsegle  31385  ellines  31429  nn0prpwlem  31487  nn0prpw  31488  ptrest  32578  ismblfin  32620  itg2addnclem3  32633  itg2addnc  32634  isline  34043  psubspi  34051  paddfval  34101  elpadd  34103  paddvaln0N  34105  mzpcompact2lem  36332  mzpcompact2  36333  sbc4rexgOLD  36372  pell1qrval  36428  elpell1qr  36429  pell14qrval  36430  elpell14qr  36431  pell1234qrval  36432  elpell1234qr  36433  jm2.27  36593  expdiophlem1  36606  clsk1independent  37364  limclner  38718  fourierdlem42  39042  fourierdlem48  39047  isgbe  40173  isgbo  40174  isgboa  40175  sgoldbalt  40203  nnsum3primesle9  40210  nb3grpr  40610  upgr4cycl4dv4e  41352  vdgn1frgrv2  41466  fusgr2wsp2nb  41498  bigoval  42141  elbigo  42143