Theorem 2rexbidv 3228

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  f1oiso  7357  elrnmpog  7553  elrnmpo  7554  ralrnmpo  7557  ovelrn  7595  mpt3fvd  7686  opiota  8068  omeu  8586  oeeui  8604  eroveu  8826  erov  8828  elfiun  9415  dffi3  9416  xpwdomg  9572  brdom7disj  10603  brdom6disj  10604  genpv  11077  genpelv  11078  axcnre  11242  supadd  12278  supmullem1  12280  supmullem2  12281  supmul  12282  01sqrexlem6  15407  ello1  15675  ello1mpt  15681  elo1  15686  lo1o1  15692  o1lo1  15697  bezoutlem1  16705  bezoutlem3  16707  bezoutlem4  16708  bezout  16709  pythagtriplem2  16988  pythagtriplem19  17004  pythagtrip  17005  pcval  17015  pceu  17017  pczpre  17018  pcdiv  17023  4sqlem2  17120  4sqlem3  17121  4sqlem4  17123  4sq  17135  vdwlem1  17152  vdwlem12  17163  vdwlem13  17164  vdwnnlem1  17166  vdwnnlem2  17167  vdwnnlem3  17168  vdwnn  17169  ramub2  17185  rami  17186  cat1lem  18264  cat1  18265  pgpfac1lem3  20286  lspprel  21362  znunit  21862  cayleyhamiltonALT  23202  hausnei  23639  isreg2  23688  txuni2  23877  txbas  23879  xkoopn  23901  txcls  23916  txcnpi  23920  txdis1cn  23947  txtube  23952  txcmplem1  23953  hausdiag  23957  tx1stc  23962  regr1lem2  24052  qustgplem  24433  met2ndci  24834  dyadmax  25912  i1fadd  26009  i1fmul  26010  elply  26506  2sqlem2  27738  2sqlem8  27746  2sqlem9  27747  2sqlem11  27749  flt4lem7  27982  nna4b4nsq  27983  elmade  28236  mulsval  28488  mulsval2lem  28489  mulsproplem9  28503  mulsproplem12  28506  sltmuls1  28526  sltmuls2  28527  mulsuniflem  28528  addsdilem2  28531  mulsasslem1  28542  mulsasslem2  28543  mulsunif2  28549  precsexlemcbv  28585  precsexlem9  28594  precsexlem11  28596  eucliddivs  28755  bdayfinbndcbv  28845  bdayfinbndlem1  28846  bdayfinbndlem2  28847  bdayfinbnd  28848  elz12s  28851  z12zsodd  28861  z12sge0  28862  remulscllem1  28879  istrkgld  28914  istrkg3ld  28916  axtgupdim2  28926  axtgeucl  28927  legov  29041  iscgra  29309  dfcgra2  29331  axsegconlem1  29488  axpasch  29512  axlowdim  29532  axeuclidlem  29533  nb3grpr  29956  upgr4cycl4dv4e  30779  vdgn1frgrv2  30890  fusgr2wsp2nb  30928  l2p  31074  br8d  33195  gsumwun  33630  constrsuc  34363  constrsslem  34366  constrconj  34370  constrllcllem  34377  constrlccllem  34378  constrcccllem  34379  constrcbvlem  34380  pstmval  34520  eulerpartlemgh  35003  eulerpartlemgs2  35005  cvmliftlem15  36042  cvmlift2lem10  36056  satf  36097  satfv0  36102  satfrnmapom  36114  satfv0fun  36115  satf0op  36121  sat1el2xp  36123  fmlafvel  36129  fmla1  36131  fmlaomn0  36134  gonan0  36136  goaln0  36137  gonar  36139  goalr  36141  fmlasucdisj  36143  satffunlem2lem1  36148  dmopab3rexdif  36149  satfv0fvfmla0  36157  sategoelfvb  36163  satfv1fvfmla1  36167  2goelgoanfmla1  36168  br8  36500  br6  36501  br4  36502  elaltxp  36720  brsegle  36853  ellines  36897  nn0prpwlem  37090  nn0prpw  37091  ptrest  38517  ismblfin  38559  itg2addnclem3  38571  itg2addnc  38572  releldmqscoss  39657  isline  40776  psubspi  40784  paddfval  40834  elpadd  40836  paddvaln0N  40838  3rspcedvd  43250  mzpcompact2lem  43741  mzpcompact2  43742  pell1qrval  43832  elpell1qr  43833  pell14qrval  43834  elpell14qr  43835  pell1234qrval  43836  elpell1234qr  43837  jm2.27  43994  expdiophlem1  44007  oenord1  44302  oaun3lem1  44360  clsk1independent  45031  limclner  46630  fourierdlem42  47128  fourierdlem48  47133  sprel  48535  prelspr  48537  prprelb  48567  prprelprb  48568  reuprpr  48574  isgbe  48818  isgbow  48819  isgbo  48820  sbgoldbalt  48848  sgoldbeven3prm  48850  mogoldbb  48852  sbgoldbo  48854  nnsum3primesle9  48861  usgrgrtrirex  49017  grlimgrtri  49070  grlimedgnedg  49198  bigoval  49630  elbigo  49632  iscnrm3r  50025  iscnrm3l  50028