Theorem 2rexbidv 3236

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  f1oiso  7350  elrnmpog  7546  elrnmpo  7547  ralrnmpo  7550  ovelrn  7587  opiota  8055  omeu  8569  oeeui  8587  eroveu  8809  erov  8811  elfiun  9389  dffi3  9390  xpwdomg  9546  brdom7disj  10514  brdom6disj  10515  genpv  10983  genpelv  10984  axcnre  11148  supadd  12182  supmullem1  12184  supmullem2  12185  supmul  12186  01sqrexlem6  15297  ello1  15565  ello1mpt  15571  elo1  15576  lo1o1  15582  o1lo1  15587  bezoutlem1  16596  bezoutlem3  16598  bezoutlem4  16599  bezout  16600  pythagtriplem2  16876  pythagtriplem19  16892  pythagtrip  16893  pcval  16903  pceu  16905  pczpre  16906  pcdiv  16911  4sqlem2  17008  4sqlem3  17009  4sqlem4  17011  4sq  17023  vdwlem1  17040  vdwlem12  17051  vdwlem13  17052  vdwnnlem1  17054  vdwnnlem2  17055  vdwnnlem3  17056  vdwnn  17057  ramub2  17073  rami  17074  cat1lem  18152  cat1  18153  pgpfac1lem3  20148  lspprel  21192  znunit  21681  cayleyhamiltonALT  23016  hausnei  23453  isreg2  23502  txuni2  23690  txbas  23692  xkoopn  23714  txcls  23729  txcnpi  23733  txdis1cn  23760  txtube  23765  txcmplem1  23766  hausdiag  23770  tx1stc  23775  regr1lem2  23865  qustgplem  24246  met2ndci  24647  dyadmax  25725  i1fadd  25822  i1fmul  25823  elply  26320  2sqlem2  27547  2sqlem8  27555  2sqlem9  27556  2sqlem11  27558  elmade  28015  mulsval  28267  mulsval2lem  28268  mulsproplem9  28282  mulsproplem12  28285  sltmuls1  28305  sltmuls2  28306  mulsuniflem  28307  addsdilem2  28310  mulsasslem1  28321  mulsasslem2  28322  mulsunif2  28328  precsexlemcbv  28364  precsexlem9  28373  precsexlem11  28375  eucliddivs  28534  bdayfinbndcbv  28624  bdayfinbndlem1  28625  bdayfinbndlem2  28626  bdayfinbnd  28627  elz12s  28630  z12zsodd  28640  z12sge0  28641  remulscllem1  28658  istrkgld  28693  istrkg3ld  28695  axtgupdim2  28705  axtgeucl  28706  legov  28819  iscgra  29076  dfcgra2  29097  axsegconlem1  29207  axpasch  29231  axlowdim  29251  axeuclidlem  29252  nb3grpr  29672  upgr4cycl4dv4e  30476  vdgn1frgrv2  30587  fusgr2wsp2nb  30625  l2p  30771  br8d  32893  gsumwun  33336  constrsuc  34072  constrsslem  34075  constrconj  34079  constrllcllem  34086  constrlccllem  34087  constrcccllem  34088  constrcbvlem  34089  pstmval  34229  eulerpartlemgh  34712  eulerpartlemgs2  34714  cvmliftlem15  35688  cvmlift2lem10  35702  satf  35743  satfv0  35748  satfrnmapom  35760  satfv0fun  35761  satf0op  35767  sat1el2xp  35769  fmlafvel  35775  fmla1  35777  fmlaomn0  35780  gonan0  35782  goaln0  35783  gonar  35785  goalr  35787  fmlasucdisj  35789  satffunlem2lem1  35794  dmopab3rexdif  35795  satfv0fvfmla0  35803  sategoelfvb  35809  satfv1fvfmla1  35813  2goelgoanfmla1  35814  br8  36146  br6  36147  br4  36148  elaltxp  36365  brsegle  36498  ellines  36542  nn0prpwlem  36721  nn0prpw  36722  ptrest  38157  ismblfin  38199  itg2addnclem3  38211  itg2addnc  38212  releldmqscoss  39283  isline  40402  psubspi  40410  paddfval  40460  elpadd  40462  paddvaln0N  40464  3rspcedvd  42876  flt4lem7  43282  nna4b4nsq  43283  mzpcompact2lem  43373  mzpcompact2  43374  pell1qrval  43464  elpell1qr  43465  pell14qrval  43466  elpell14qr  43467  pell1234qrval  43468  elpell1234qr  43469  jm2.27  43626  expdiophlem1  43639  oenord1  43934  oaun3lem1  43992  clsk1independent  44663  limclner  46256  fourierdlem42  46754  fourierdlem48  46759  sprel  48121  prelspr  48123  prprelb  48153  prprelprb  48154  reuprpr  48160  isgbe  48404  isgbow  48405  isgbo  48406  sbgoldbalt  48434  sgoldbeven3prm  48436  mogoldbb  48438  sbgoldbo  48440  nnsum3primesle9  48447  usgrgrtrirex  48603  grlimgrtri  48656  grlimedgnedg  48784  bigoval  49213  elbigo  49215  iscnrm3r  49610  iscnrm3l  49613