Theorem 2rexbidv 3203

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  f1oiso  7307  elrnmpog  7503  elrnmpo  7504  ralrnmpo  7507  ovelrn  7544  opiota  8013  omeu  8522  oeeui  8540  eroveu  8761  erov  8763  elfiun  9345  dffi3  9346  xpwdomg  9502  brdom7disj  10453  brdom6disj  10454  genpv  10922  genpelv  10923  axcnre  11087  supadd  12122  supmullem1  12124  supmullem2  12125  supmul  12126  01sqrexlem6  15182  ello1  15450  ello1mpt  15456  elo1  15461  lo1o1  15467  o1lo1  15472  bezoutlem1  16478  bezoutlem3  16480  bezoutlem4  16481  bezout  16482  pythagtriplem2  16757  pythagtriplem19  16773  pythagtrip  16774  pcval  16784  pceu  16786  pczpre  16787  pcdiv  16792  4sqlem2  16889  4sqlem3  16890  4sqlem4  16892  4sq  16904  vdwlem1  16921  vdwlem12  16932  vdwlem13  16933  vdwnnlem1  16935  vdwnnlem2  16936  vdwnnlem3  16937  vdwnn  16938  ramub2  16954  rami  16955  cat1lem  18032  cat1  18033  pgpfac1lem3  20020  lspprel  21058  znunit  21530  cayleyhamiltonALT  22847  hausnei  23284  isreg2  23333  txuni2  23521  txbas  23523  xkoopn  23545  txcls  23560  txcnpi  23564  txdis1cn  23591  txtube  23596  txcmplem1  23597  hausdiag  23601  tx1stc  23606  regr1lem2  23696  qustgplem  24077  met2ndci  24478  dyadmax  25567  i1fadd  25664  i1fmul  25665  elply  26168  2sqlem2  27397  2sqlem8  27405  2sqlem9  27406  2sqlem11  27408  elmade  27865  mulsval  28117  mulsval2lem  28118  mulsproplem9  28132  mulsproplem12  28135  sltmuls1  28155  sltmuls2  28156  mulsuniflem  28157  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  mulsunif2  28178  precsexlemcbv  28214  precsexlem9  28223  precsexlem11  28225  eucliddivs  28384  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  bdayfinbnd  28477  elz12s  28480  z12zsodd  28490  z12sge0  28491  remulscllem1  28508  istrkgld  28543  istrkg3ld  28545  axtgupdim2  28555  axtgeucl  28556  legov  28669  iscgra  28893  dfcgra2  28914  axsegconlem1  29002  axpasch  29026  axlowdim  29046  axeuclidlem  29047  nb3grpr  29467  upgr4cycl4dv4e  30272  vdgn1frgrv2  30383  fusgr2wsp2nb  30421  l2p  30567  br8d  32698  gsumwun  33170  constrsuc  33916  constrsslem  33919  constrconj  33923  constrllcllem  33930  constrlccllem  33931  constrcccllem  33932  constrcbvlem  33933  pstmval  34073  eulerpartlemgh  34556  eulerpartlemgs2  34558  cvmliftlem15  35514  cvmlift2lem10  35528  satf  35569  satfv0  35574  satfrnmapom  35586  satfv0fun  35587  satf0op  35593  sat1el2xp  35595  fmlafvel  35601  fmla1  35603  fmlaomn0  35606  gonan0  35608  goaln0  35609  gonar  35611  goalr  35613  fmlasucdisj  35615  satffunlem2lem1  35620  dmopab3rexdif  35621  satfv0fvfmla0  35629  sategoelfvb  35635  satfv1fvfmla1  35639  2goelgoanfmla1  35640  br8  35972  br6  35973  br4  35974  elaltxp  36191  brsegle  36324  ellines  36368  nn0prpwlem  36538  nn0prpw  36539  ptrest  37870  ismblfin  37912  itg2addnclem3  37924  itg2addnc  37925  releldmqscoss  38996  isline  40115  psubspi  40123  paddfval  40173  elpadd  40175  paddvaln0N  40177  3rspcedvd  42588  flt4lem7  43017  nna4b4nsq  43018  mzpcompact2lem  43108  mzpcompact2  43109  sbc4rexgOLD  43147  pell1qrval  43203  elpell1qr  43204  pell14qrval  43205  elpell14qr  43206  pell1234qrval  43207  elpell1234qr  43208  jm2.27  43365  expdiophlem1  43378  oenord1  43673  oaun3lem1  43731  clsk1independent  44402  limclner  46009  fourierdlem42  46507  fourierdlem48  46512  sprel  47844  prelspr  47846  prprelb  47876  prprelprb  47877  reuprpr  47883  isgbe  48111  isgbow  48112  isgbo  48113  sbgoldbalt  48141  sgoldbeven3prm  48143  mogoldbb  48145  sbgoldbo  48147  nnsum3primesle9  48154  usgrgrtrirex  48310  grlimgrtri  48363  grlimedgnedg  48491  bigoval  48909  elbigo  48911  iscnrm3r  49307  iscnrm3l  49310