Theorem 2rexbidv 3230

Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)

Hypothesis

Ref	Expression
2rexbidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
2rexbidv	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidv

Step	Hyp	Ref	Expression
1		2rexbidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	rexbidv 3227	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒))
3	2	rexbidv 3227	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ↔ wb 205  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3071

This theorem is referenced by:  f1oiso  7231  elrnmpog  7418  elrnmpo  7419  ralrnmpo  7421  ovelrn  7457  opiota  7908  omeu  8425  oeeui  8442  eroveu  8610  erov  8612  elfiun  9198  dffi3  9199  xpwdomg  9353  brdom7disj  10296  brdom6disj  10297  genpv  10764  genpelv  10765  axcnre  10929  supadd  11952  supmullem1  11954  supmullem2  11955  supmul  11956  sqrlem6  14968  ello1  15233  ello1mpt  15239  elo1  15244  lo1o1  15250  o1lo1  15255  bezoutlem1  16256  bezoutlem3  16258  bezoutlem4  16259  bezout  16260  pythagtriplem2  16527  pythagtriplem19  16543  pythagtrip  16544  pcval  16554  pceu  16556  pczpre  16557  pcdiv  16562  4sqlem2  16659  4sqlem3  16660  4sqlem4  16662  4sq  16674  vdwlem1  16691  vdwlem12  16702  vdwlem13  16703  vdwnnlem1  16705  vdwnnlem2  16706  vdwnnlem3  16707  vdwnn  16708  ramub2  16724  rami  16725  cat1lem  17820  cat1  17821  pgpfac1lem3  19689  lspprel  20365  znunit  20780  cayleyhamiltonALT  22049  hausnei  22488  isreg2  22537  txuni2  22725  txbas  22727  xkoopn  22749  txcls  22764  txcnpi  22768  txdis1cn  22795  txtube  22800  txcmplem1  22801  hausdiag  22805  tx1stc  22810  regr1lem2  22900  qustgplem  23281  met2ndci  23687  dyadmax  24771  i1fadd  24868  i1fmul  24869  elply  25365  2sqlem2  26575  2sqlem8  26583  2sqlem9  26584  2sqlem11  26586  istrkgld  26829  istrkg3ld  26831  axtgupdim2  26841  axtgeucl  26842  legov  26955  iscgra  27179  dfcgra2  27200  axsegconlem1  27294  axpasch  27318  axlowdim  27338  axeuclidlem  27339  nb3grpr  27758  upgr4cycl4dv4e  28558  vdgn1frgrv2  28669  fusgr2wsp2nb  28707  l2p  28850  br8d  30959  pstmval  31854  eulerpartlemgh  32354  eulerpartlemgs2  32356  cvmliftlem15  33269  cvmlift2lem10  33283  satf  33324  satfv0  33329  satfrnmapom  33341  satfv0fun  33342  satf0op  33348  sat1el2xp  33350  fmlafvel  33356  fmla1  33358  fmlaomn0  33361  gonan0  33363  goaln0  33364  gonar  33366  goalr  33368  fmlasucdisj  33370  satffunlem2lem1  33375  dmopab3rexdif  33376  satfv0fvfmla0  33384  sategoelfvb  33390  satfv1fvfmla1  33394  2goelgoanfmla1  33395  br8  33732  br6  33733  br4  33734  elmade  34060  elaltxp  34286  brsegle  34419  ellines  34463  nn0prpwlem  34520  nn0prpw  34521  ptrest  35785  ismblfin  35827  itg2addnclem3  35839  itg2addnc  35840  releldmqscoss  36779  isline  37760  psubspi  37768  paddfval  37818  elpadd  37820  paddvaln0N  37822  3rspcedvd  40189  flt4lem7  40503  nna4b4nsq  40504  mzpcompact2lem  40580  mzpcompact2  40581  sbc4rexgOLD  40619  pell1qrval  40675  elpell1qr  40676  pell14qrval  40677  elpell14qr  40678  pell1234qrval  40679  elpell1234qr  40680  jm2.27  40837  expdiophlem1  40850  clsk1independent  41663  limclner  43199  fourierdlem42  43697  fourierdlem48  43702  sprel  44947  prelspr  44949  prprelb  44979  prprelprb  44980  reuprpr  44986  isgbe  45214  isgbow  45215  isgbo  45216  sbgoldbalt  45244  sgoldbeven3prm  45246  mogoldbb  45248  sbgoldbo  45250  nnsum3primesle9  45257  bigoval  45906  elbigo  45908  iscnrm3r  46253  iscnrm3l  46256