Theorem 2rexbidv 3227

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  f1oiso  7363  elrnmpog  7559  elrnmpo  7560  ralrnmpo  7563  ovelrn  7601  mpt3fvd  7692  opiota  8075  omeu  8601  oeeui  8619  eroveu  8841  erov  8843  elfiun  9429  dffi3  9430  xpwdomg  9586  brdom7disj  10617  brdom6disj  10618  genpv  11091  genpelv  11092  axcnre  11256  supadd  12292  supmullem1  12294  supmullem2  12295  supmul  12296  01sqrexlem6  15423  ello1  15691  ello1mpt  15697  elo1  15702  lo1o1  15708  o1lo1  15713  bezoutlem1  16721  bezoutlem3  16723  bezoutlem4  16724  bezout  16725  pythagtriplem2  17004  pythagtriplem19  17020  pythagtrip  17021  pcval  17031  pceu  17033  pczpre  17034  pcdiv  17039  4sqlem2  17136  4sqlem3  17137  4sqlem4  17139  4sq  17151  vdwlem1  17168  vdwlem12  17179  vdwlem13  17180  vdwnnlem1  17182  vdwnnlem2  17183  vdwnnlem3  17184  vdwnn  17185  ramub2  17201  rami  17202  cat1lem  18280  cat1  18281  pgpfac1lem3  20302  lspprel  21378  znunit  21878  cayleyhamiltonALT  23218  hausnei  23655  isreg2  23704  txuni2  23893  txbas  23895  xkoopn  23917  txcls  23932  txcnpi  23936  txdis1cn  23963  txtube  23968  txcmplem1  23969  hausdiag  23973  tx1stc  23978  regr1lem2  24068  qustgplem  24449  met2ndci  24850  dyadmax  25928  i1fadd  26025  i1fmul  26026  elply  26522  2sqlem2  27754  2sqlem8  27762  2sqlem9  27763  2sqlem11  27765  flt4lem7  27998  nna4b4nsq  27999  elmade  28252  mulsval  28504  mulsval2lem  28505  mulsproplem9  28519  mulsproplem12  28522  sltmuls1  28542  sltmuls2  28543  mulsuniflem  28544  addsdilem2  28547  mulsasslem1  28558  mulsasslem2  28559  mulsunif2  28565  precsexlemcbv  28601  precsexlem9  28610  precsexlem11  28612  eucliddivs  28771  bdayfinbndcbv  28861  bdayfinbndlem1  28862  bdayfinbndlem2  28863  bdayfinbnd  28864  elz12s  28867  z12zsodd  28877  z12sge0  28878  remulscllem1  28895  istrkgld  28930  istrkg3ld  28932  axtgupdim2  28942  axtgeucl  28943  legov  29057  iscgra  29325  dfcgra2  29347  axsegconlem1  29504  axpasch  29528  axlowdim  29548  axeuclidlem  29549  nb3grpr  29972  upgr4cycl4dv4e  30795  vdgn1frgrv2  30906  fusgr2wsp2nb  30944  l2p  31090  br8d  33253  gsumwun  33687  constrsuc  34420  constrsslem  34423  constrconj  34427  constrllcllem  34434  constrlccllem  34435  constrcccllem  34436  constrcbvlem  34437  pstmval  34577  eulerpartlemgh  35060  eulerpartlemgs2  35062  omeueq  35773  cvmliftlem15  36181  cvmlift2lem10  36195  satf  36236  satfv0  36241  satfrnmapom  36253  satfv0fun  36254  satf0op  36260  sat1el2xp  36262  fmlafvel  36268  fmla1  36270  fmlaomn0  36273  gonan0  36275  goaln0  36276  gonar  36278  goalr  36280  fmlasucdisj  36282  satffunlem2lem1  36287  dmopab3rexdif  36288  satfv0fvfmla0  36296  sategoelfvb  36302  satfv1fvfmla1  36306  2goelgoanfmla1  36307  br8  36645  br6  36646  br4  36647  elaltxp  36864  brsegle  36997  ellines  37041  nn0prpwlem  37234  nn0prpw  37235  ptrest  38674  ismblfin  38716  itg2addnclem3  38728  itg2addnc  38729  releldmqscoss  39814  isline  40933  psubspi  40941  paddfval  40991  elpadd  40993  paddvaln0N  40995  3rspcedvd  43407  mzpcompact2lem  43899  mzpcompact2  43900  pell1qrval  43990  elpell1qr  43991  pell14qrval  43992  elpell14qr  43993  pell1234qrval  43994  elpell1234qr  43995  jm2.27  44152  expdiophlem1  44165  oenord1  44455  oaun3lem1  44513  clsk1independent  45183  limclner  46797  fourierdlem42  47295  fourierdlem48  47300  sprel  48702  prelspr  48704  prprelb  48734  prprelprb  48735  reuprpr  48741  isgbe  48985  isgbow  48986  isgbo  48987  sbgoldbalt  49015  sgoldbeven3prm  49017  mogoldbb  49019  sbgoldbo  49021  nnsum3primesle9  49028  usgrgrtrirex  49184  grlimgrtri  49237  grlimedgnedg  49365  bigoval  49797  elbigo  49799  iscnrm3r  50198  iscnrm3l  50201  fuconuniqex2  50923