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 1828  ax-4 1842  ax-5 1943

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

This theorem is used by:  f1oiso  7352  elrnmpog  7548  elrnmpo  7549  ralrnmpo  7552  ovelrn  7590  opiota  8056  omeu  8572  oeeui  8590  eroveu  8812  erov  8814  elfiun  9400  dffi3  9401  xpwdomg  9557  brdom7disj  10534  brdom6disj  10535  genpv  11008  genpelv  11009  axcnre  11173  supadd  12207  supmullem1  12209  supmullem2  12210  supmul  12211  01sqrexlem6  15334  ello1  15602  ello1mpt  15608  elo1  15613  lo1o1  15619  o1lo1  15624  bezoutlem1  16629  bezoutlem3  16631  bezoutlem4  16632  bezout  16633  pythagtriplem2  16909  pythagtriplem19  16925  pythagtrip  16926  pcval  16936  pceu  16938  pczpre  16939  pcdiv  16944  4sqlem2  17041  4sqlem3  17042  4sqlem4  17044  4sq  17056  vdwlem1  17073  vdwlem12  17084  vdwlem13  17085  vdwnnlem1  17087  vdwnnlem2  17088  vdwnnlem3  17089  vdwnn  17090  ramub2  17106  rami  17107  cat1lem  18185  cat1  18186  pgpfac1lem3  20206  lspprel  21278  znunit  21776  cayleyhamiltonALT  23116  hausnei  23553  isreg2  23602  txuni2  23791  txbas  23793  xkoopn  23815  txcls  23830  txcnpi  23834  txdis1cn  23861  txtube  23866  txcmplem1  23867  hausdiag  23871  tx1stc  23876  regr1lem2  23966  qustgplem  24347  met2ndci  24748  dyadmax  25826  i1fadd  25923  i1fmul  25924  elply  26420  2sqlem2  27654  2sqlem8  27662  2sqlem9  27663  2sqlem11  27665  elmade  28122  mulsval  28374  mulsval2lem  28375  mulsproplem9  28389  mulsproplem12  28392  sltmuls1  28412  sltmuls2  28413  mulsuniflem  28414  addsdilem2  28417  mulsasslem1  28428  mulsasslem2  28429  mulsunif2  28435  precsexlemcbv  28471  precsexlem9  28480  precsexlem11  28482  eucliddivs  28641  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  bdayfinbnd  28734  elz12s  28737  z12zsodd  28747  z12sge0  28748  remulscllem1  28765  istrkgld  28800  istrkg3ld  28802  axtgupdim2  28812  axtgeucl  28813  legov  28927  iscgra  29195  dfcgra2  29217  axsegconlem1  29374  axpasch  29398  axlowdim  29418  axeuclidlem  29419  nb3grpr  29842  upgr4cycl4dv4e  30665  vdgn1frgrv2  30776  fusgr2wsp2nb  30814  l2p  30960  br8d  33081  gsumwun  33516  constrsuc  34248  constrsslem  34251  constrconj  34255  constrllcllem  34262  constrlccllem  34263  constrcccllem  34264  constrcbvlem  34265  pstmval  34405  eulerpartlemgh  34889  eulerpartlemgs2  34891  cvmliftlem15  35877  cvmlift2lem10  35891  satf  35932  satfv0  35937  satfrnmapom  35949  satfv0fun  35950  satf0op  35956  sat1el2xp  35958  fmlafvel  35964  fmla1  35966  fmlaomn0  35969  gonan0  35971  goaln0  35972  gonar  35974  goalr  35976  fmlasucdisj  35978  satffunlem2lem1  35983  dmopab3rexdif  35984  satfv0fvfmla0  35992  sategoelfvb  35998  satfv1fvfmla1  36002  2goelgoanfmla1  36003  br8  36335  br6  36336  br4  36337  elaltxp  36555  brsegle  36688  ellines  36732  nn0prpwlem  36941  nn0prpw  36942  ptrest  38368  ismblfin  38410  itg2addnclem3  38422  itg2addnc  38423  releldmqscoss  39493  isline  40612  psubspi  40620  paddfval  40670  elpadd  40672  paddvaln0N  40674  3rspcedvd  43086  flt4lem7  43505  nna4b4nsq  43506  mzpcompact2lem  43596  mzpcompact2  43597  pell1qrval  43687  elpell1qr  43688  pell14qrval  43689  elpell14qr  43690  pell1234qrval  43691  elpell1234qr  43692  jm2.27  43849  expdiophlem1  43862  oenord1  44157  oaun3lem1  44215  clsk1independent  44886  limclner  46479  fourierdlem42  46977  fourierdlem48  46982  sprel  48384  prelspr  48386  prprelb  48416  prprelprb  48417  reuprpr  48423  isgbe  48667  isgbow  48668  isgbo  48669  sbgoldbalt  48697  sgoldbeven3prm  48699  mogoldbb  48701  sbgoldbo  48703  nnsum3primesle9  48710  usgrgrtrirex  48866  grlimgrtri  48919  grlimedgnedg  49047  bigoval  49479  elbigo  49481  iscnrm3r  49874  iscnrm3l  49877