Theorem 2rexbidv 3302

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

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

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 3146

This theorem is referenced by:  f1oiso  7106  elrnmpog  7288  elrnmpo  7289  ralrnmpo  7291  ovelrn  7326  opiota  7759  omeu  8213  oeeui  8230  eroveu  8394  erov  8396  elfiun  8896  dffi3  8897  xpwdomg  9051  brdom7disj  9955  brdom6disj  9956  genpv  10423  genpelv  10424  axcnre  10588  supadd  11611  supmullem1  11613  supmullem2  11614  supmul  11615  sqrlem6  14609  ello1  14874  ello1mpt  14880  elo1  14885  lo1o1  14891  o1lo1  14896  bezoutlem1  15889  bezoutlem3  15891  bezoutlem4  15892  bezout  15893  pythagtriplem2  16156  pythagtriplem19  16172  pythagtrip  16173  pcval  16183  pceu  16185  pczpre  16186  pcdiv  16191  4sqlem2  16287  4sqlem3  16288  4sqlem4  16290  4sq  16302  vdwlem1  16319  vdwlem12  16330  vdwlem13  16331  vdwnnlem1  16333  vdwnnlem2  16334  vdwnnlem3  16335  vdwnn  16336  ramub2  16352  rami  16353  pgpfac1lem3  19201  lspprel  19868  znunit  20712  cayleyhamiltonALT  21501  hausnei  21938  isreg2  21987  txuni2  22175  txbas  22177  xkoopn  22199  txcls  22214  txcnpi  22218  txdis1cn  22245  txtube  22250  txcmplem1  22251  hausdiag  22255  tx1stc  22260  regr1lem2  22350  qustgplem  22731  met2ndci  23134  dyadmax  24201  i1fadd  24298  i1fmul  24299  elply  24787  2sqlem2  25996  2sqlem8  26004  2sqlem9  26005  2sqlem11  26007  istrkgld  26247  istrkg3ld  26249  axtgupdim2  26259  axtgeucl  26260  legov  26373  iscgra  26597  dfcgra2  26618  axsegconlem1  26705  axpasch  26729  axlowdim  26749  axeuclidlem  26750  nb3grpr  27166  upgr4cycl4dv4e  27966  vdgn1frgrv2  28077  fusgr2wsp2nb  28115  l2p  28258  br8d  30363  pstmval  31137  eulerpartlemgh  31638  eulerpartlemgs2  31640  cvmliftlem15  32547  cvmlift2lem10  32561  satf  32602  satfv0  32607  satfrnmapom  32619  satfv0fun  32620  satf0op  32626  sat1el2xp  32628  fmlafvel  32634  fmla1  32636  fmlaomn0  32639  gonan0  32641  goaln0  32642  gonar  32644  goalr  32646  fmlasucdisj  32648  satffunlem2lem1  32653  dmopab3rexdif  32654  satfv0fvfmla0  32662  sategoelfvb  32668  satfv1fvfmla1  32672  2goelgoanfmla1  32673  br8  32994  br6  32995  br4  32996  elaltxp  33438  brsegle  33571  ellines  33615  nn0prpwlem  33672  nn0prpw  33673  ptrest  34893  ismblfin  34935  itg2addnclem3  34947  itg2addnc  34948  releldmqscoss  35896  isline  36877  psubspi  36885  paddfval  36935  elpadd  36937  paddvaln0N  36939  3rspcedvd  39112  mzpcompact2lem  39355  mzpcompact2  39356  sbc4rexgOLD  39394  pell1qrval  39450  elpell1qr  39451  pell14qrval  39452  elpell14qr  39453  pell1234qrval  39454  elpell1234qr  39455  jm2.27  39612  expdiophlem1  39625  clsk1independent  40403  limclner  41939  fourierdlem42  42441  fourierdlem48  42446  sprel  43653  prelspr  43655  prprelb  43685  prprelprb  43686  reuprpr  43692  isgbe  43923  isgbow  43924  isgbo  43925  sbgoldbalt  43953  sgoldbeven3prm  43955  mogoldbb  43957  sbgoldbo  43959  nnsum3primesle9  43966  bigoval  44616  elbigo  44618