Theorem 2rexbidv 3194

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 3153	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3153	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  7288  elrnmpog  7484  elrnmpo  7485  ralrnmpo  7488  ovelrn  7525  opiota  7994  omeu  8503  oeeui  8520  eroveu  8739  erov  8741  elfiun  9320  dffi3  9321  xpwdomg  9477  brdom7disj  10425  brdom6disj  10426  genpv  10893  genpelv  10894  axcnre  11058  supadd  12093  supmullem1  12095  supmullem2  12096  supmul  12097  01sqrexlem6  15154  ello1  15422  ello1mpt  15428  elo1  15433  lo1o1  15439  o1lo1  15444  bezoutlem1  16450  bezoutlem3  16452  bezoutlem4  16453  bezout  16454  pythagtriplem2  16729  pythagtriplem19  16745  pythagtrip  16746  pcval  16756  pceu  16758  pczpre  16759  pcdiv  16764  4sqlem2  16861  4sqlem3  16862  4sqlem4  16864  4sq  16876  vdwlem1  16893  vdwlem12  16904  vdwlem13  16905  vdwnnlem1  16907  vdwnnlem2  16908  vdwnnlem3  16909  vdwnn  16910  ramub2  16926  rami  16927  cat1lem  18003  cat1  18004  pgpfac1lem3  19958  lspprel  20998  znunit  21470  cayleyhamiltonALT  22776  hausnei  23213  isreg2  23262  txuni2  23450  txbas  23452  xkoopn  23474  txcls  23489  txcnpi  23493  txdis1cn  23520  txtube  23525  txcmplem1  23526  hausdiag  23530  tx1stc  23535  regr1lem2  23625  qustgplem  24006  met2ndci  24408  dyadmax  25497  i1fadd  25594  i1fmul  25595  elply  26098  2sqlem2  27327  2sqlem8  27335  2sqlem9  27336  2sqlem11  27338  elmade  27781  mulsval  28017  mulsval2lem  28018  mulsproplem9  28032  mulsproplem12  28035  ssltmul1  28055  ssltmul2  28056  mulsuniflem  28057  addsdilem2  28060  mulsasslem1  28071  mulsasslem2  28072  mulsunif2  28078  precsexlemcbv  28113  precsexlem9  28122  precsexlem11  28124  eucliddivs  28270  elzs12  28350  zs12zodd  28359  zs12ge0  28360  remulscllem1  28369  istrkgld  28404  istrkg3ld  28406  axtgupdim2  28416  axtgeucl  28417  legov  28530  iscgra  28754  dfcgra2  28775  axsegconlem1  28862  axpasch  28886  axlowdim  28906  axeuclidlem  28907  nb3grpr  29327  upgr4cycl4dv4e  30129  vdgn1frgrv2  30240  fusgr2wsp2nb  30278  l2p  30423  br8d  32555  gsumwun  33018  constrsuc  33705  constrsslem  33708  constrconj  33712  constrllcllem  33719  constrlccllem  33720  constrcccllem  33721  constrcbvlem  33722  pstmval  33862  eulerpartlemgh  34346  eulerpartlemgs2  34348  cvmliftlem15  35271  cvmlift2lem10  35285  satf  35326  satfv0  35331  satfrnmapom  35343  satfv0fun  35344  satf0op  35350  sat1el2xp  35352  fmlafvel  35358  fmla1  35360  fmlaomn0  35363  gonan0  35365  goaln0  35366  gonar  35368  goalr  35370  fmlasucdisj  35372  satffunlem2lem1  35377  dmopab3rexdif  35378  satfv0fvfmla0  35386  sategoelfvb  35392  satfv1fvfmla1  35396  2goelgoanfmla1  35397  br8  35729  br6  35730  br4  35731  elaltxp  35949  brsegle  36082  ellines  36126  nn0prpwlem  36296  nn0prpw  36297  ptrest  37599  ismblfin  37641  itg2addnclem3  37653  itg2addnc  37654  releldmqscoss  38638  isline  39718  psubspi  39726  paddfval  39776  elpadd  39778  paddvaln0N  39780  3rspcedvd  42188  flt4lem7  42632  nna4b4nsq  42633  mzpcompact2lem  42724  mzpcompact2  42725  sbc4rexgOLD  42763  pell1qrval  42819  elpell1qr  42820  pell14qrval  42821  elpell14qr  42822  pell1234qrval  42823  elpell1234qr  42824  jm2.27  42981  expdiophlem1  42994  oenord1  43289  oaun3lem1  43347  clsk1independent  44019  limclner  45632  fourierdlem42  46130  fourierdlem48  46135  sprel  47468  prelspr  47470  prprelb  47500  prprelprb  47501  reuprpr  47507  isgbe  47735  isgbow  47736  isgbo  47737  sbgoldbalt  47765  sgoldbeven3prm  47767  mogoldbb  47769  sbgoldbo  47771  nnsum3primesle9  47778  usgrgrtrirex  47934  grlimgrtri  47987  grlimedgnedg  48115  bigoval  48534  elbigo  48536  iscnrm3r  48932  iscnrm3l  48935