Theorem 2rexbidv 3230

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  f1oiso  7349  elrnmpog  7545  elrnmpo  7546  ralrnmpo  7549  ovelrn  7586  opiota  8052  omeu  8566  oeeui  8584  eroveu  8806  erov  8808  elfiun  9386  dffi3  9387  xpwdomg  9543  brdom7disj  10510  brdom6disj  10511  genpv  10979  genpelv  10980  axcnre  11144  supadd  12178  supmullem1  12180  supmullem2  12181  supmul  12182  01sqrexlem6  15294  ello1  15562  ello1mpt  15568  elo1  15573  lo1o1  15579  o1lo1  15584  bezoutlem1  16592  bezoutlem3  16594  bezoutlem4  16595  bezout  16596  pythagtriplem2  16872  pythagtriplem19  16888  pythagtrip  16889  pcval  16899  pceu  16901  pczpre  16902  pcdiv  16907  4sqlem2  17004  4sqlem3  17005  4sqlem4  17007  4sq  17019  vdwlem1  17036  vdwlem12  17047  vdwlem13  17048  vdwnnlem1  17050  vdwnnlem2  17051  vdwnnlem3  17052  vdwnn  17053  ramub2  17069  rami  17070  cat1lem  18148  cat1  18149  pgpfac1lem3  20144  lspprel  21215  znunit  21713  cayleyhamiltonALT  23048  hausnei  23485  isreg2  23534  txuni2  23722  txbas  23724  xkoopn  23746  txcls  23761  txcnpi  23765  txdis1cn  23792  txtube  23797  txcmplem1  23798  hausdiag  23802  tx1stc  23807  regr1lem2  23897  qustgplem  24278  met2ndci  24679  dyadmax  25757  i1fadd  25854  i1fmul  25855  elply  26352  2sqlem2  27582  2sqlem8  27590  2sqlem9  27591  2sqlem11  27593  elmade  28050  mulsval  28302  mulsval2lem  28303  mulsproplem9  28317  mulsproplem12  28320  sltmuls1  28340  sltmuls2  28341  mulsuniflem  28342  addsdilem2  28345  mulsasslem1  28356  mulsasslem2  28357  mulsunif2  28363  precsexlemcbv  28399  precsexlem9  28408  precsexlem11  28410  eucliddivs  28569  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  bdayfinbnd  28662  elz12s  28665  z12zsodd  28675  z12sge0  28676  remulscllem1  28693  istrkgld  28728  istrkg3ld  28730  axtgupdim2  28740  axtgeucl  28741  legov  28854  iscgra  29120  dfcgra2  29141  axsegconlem1  29267  axpasch  29291  axlowdim  29311  axeuclidlem  29312  nb3grpr  29732  upgr4cycl4dv4e  30536  vdgn1frgrv2  30647  fusgr2wsp2nb  30685  l2p  30831  br8d  32953  gsumwun  33396  constrsuc  34128  constrsslem  34131  constrconj  34135  constrllcllem  34142  constrlccllem  34143  constrcccllem  34144  constrcbvlem  34145  pstmval  34285  eulerpartlemgh  34768  eulerpartlemgs2  34770  cvmliftlem15  35790  cvmlift2lem10  35804  satf  35845  satfv0  35850  satfrnmapom  35862  satfv0fun  35863  satf0op  35869  sat1el2xp  35871  fmlafvel  35877  fmla1  35879  fmlaomn0  35882  gonan0  35884  goaln0  35885  gonar  35887  goalr  35889  fmlasucdisj  35891  satffunlem2lem1  35896  dmopab3rexdif  35897  satfv0fvfmla0  35905  sategoelfvb  35911  satfv1fvfmla1  35915  2goelgoanfmla1  35916  br8  36248  br6  36249  br4  36250  elaltxp  36467  brsegle  36600  ellines  36644  nn0prpwlem  36833  nn0prpw  36834  ptrest  38270  ismblfin  38312  itg2addnclem3  38324  itg2addnc  38325  releldmqscoss  39394  isline  40513  psubspi  40521  paddfval  40571  elpadd  40573  paddvaln0N  40575  3rspcedvd  42987  flt4lem7  43391  nna4b4nsq  43392  mzpcompact2lem  43482  mzpcompact2  43483  pell1qrval  43573  elpell1qr  43574  pell14qrval  43575  elpell14qr  43576  pell1234qrval  43577  elpell1234qr  43578  jm2.27  43735  expdiophlem1  43748  oenord1  44043  oaun3lem1  44101  clsk1independent  44772  limclner  46365  fourierdlem42  46863  fourierdlem48  46868  sprel  48233  prelspr  48235  prprelb  48265  prprelprb  48266  reuprpr  48272  isgbe  48516  isgbow  48517  isgbo  48518  sbgoldbalt  48546  sgoldbeven3prm  48548  mogoldbb  48550  sbgoldbo  48552  nnsum3primesle9  48559  usgrgrtrirex  48715  grlimgrtri  48768  grlimedgnedg  48896  bigoval  49329  elbigo  49331  iscnrm3r  49726  iscnrm3l  49729