Theorem 2rexbidv 3200

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

Syntax hints:   → wi 4   ↔ wb 206  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  f1oiso  7308  elrnmpog  7504  elrnmpo  7505  ralrnmpo  7508  ovelrn  7545  opiota  8017  omeu  8526  oeeui  8543  eroveu  8762  erov  8764  elfiun  9357  dffi3  9358  xpwdomg  9514  brdom7disj  10460  brdom6disj  10461  genpv  10928  genpelv  10929  axcnre  11093  supadd  12127  supmullem1  12129  supmullem2  12130  supmul  12131  01sqrexlem6  15189  ello1  15457  ello1mpt  15463  elo1  15468  lo1o1  15474  o1lo1  15479  bezoutlem1  16485  bezoutlem3  16487  bezoutlem4  16488  bezout  16489  pythagtriplem2  16764  pythagtriplem19  16780  pythagtrip  16781  pcval  16791  pceu  16793  pczpre  16794  pcdiv  16799  4sqlem2  16896  4sqlem3  16897  4sqlem4  16899  4sq  16911  vdwlem1  16928  vdwlem12  16939  vdwlem13  16940  vdwnnlem1  16942  vdwnnlem2  16943  vdwnnlem3  16944  vdwnn  16945  ramub2  16961  rami  16962  cat1lem  18038  cat1  18039  pgpfac1lem3  19993  lspprel  21033  znunit  21505  cayleyhamiltonALT  22811  hausnei  23248  isreg2  23297  txuni2  23485  txbas  23487  xkoopn  23509  txcls  23524  txcnpi  23528  txdis1cn  23555  txtube  23560  txcmplem1  23561  hausdiag  23565  tx1stc  23570  regr1lem2  23660  qustgplem  24041  met2ndci  24443  dyadmax  25532  i1fadd  25629  i1fmul  25630  elply  26133  2sqlem2  27362  2sqlem8  27370  2sqlem9  27371  2sqlem11  27373  elmade  27816  mulsval  28052  mulsval2lem  28053  mulsproplem9  28067  mulsproplem12  28070  ssltmul1  28090  ssltmul2  28091  mulsuniflem  28092  addsdilem2  28095  mulsasslem1  28106  mulsasslem2  28107  mulsunif2  28113  precsexlemcbv  28148  precsexlem9  28157  precsexlem11  28159  eucliddivs  28305  elzs12  28385  zs12zodd  28394  zs12ge0  28395  remulscllem1  28404  istrkgld  28439  istrkg3ld  28441  axtgupdim2  28451  axtgeucl  28452  legov  28565  iscgra  28789  dfcgra2  28810  axsegconlem1  28897  axpasch  28921  axlowdim  28941  axeuclidlem  28942  nb3grpr  29362  upgr4cycl4dv4e  30164  vdgn1frgrv2  30275  fusgr2wsp2nb  30313  l2p  30458  br8d  32588  gsumwun  33048  constrsuc  33721  constrsslem  33724  constrconj  33728  constrllcllem  33735  constrlccllem  33736  constrcccllem  33737  constrcbvlem  33738  pstmval  33878  eulerpartlemgh  34362  eulerpartlemgs2  34364  cvmliftlem15  35278  cvmlift2lem10  35292  satf  35333  satfv0  35338  satfrnmapom  35350  satfv0fun  35351  satf0op  35357  sat1el2xp  35359  fmlafvel  35365  fmla1  35367  fmlaomn0  35370  gonan0  35372  goaln0  35373  gonar  35375  goalr  35377  fmlasucdisj  35379  satffunlem2lem1  35384  dmopab3rexdif  35385  satfv0fvfmla0  35393  sategoelfvb  35399  satfv1fvfmla1  35403  2goelgoanfmla1  35404  br8  35736  br6  35737  br4  35738  elaltxp  35956  brsegle  36089  ellines  36133  nn0prpwlem  36303  nn0prpw  36304  ptrest  37606  ismblfin  37648  itg2addnclem3  37660  itg2addnc  37661  releldmqscoss  38645  isline  39726  psubspi  39734  paddfval  39784  elpadd  39786  paddvaln0N  39788  3rspcedvd  42196  flt4lem7  42640  nna4b4nsq  42641  mzpcompact2lem  42732  mzpcompact2  42733  sbc4rexgOLD  42771  pell1qrval  42827  elpell1qr  42828  pell14qrval  42829  elpell14qr  42830  pell1234qrval  42831  elpell1234qr  42832  jm2.27  42990  expdiophlem1  43003  oenord1  43298  oaun3lem1  43356  clsk1independent  44028  limclner  45642  fourierdlem42  46140  fourierdlem48  46145  sprel  47478  prelspr  47480  prprelb  47510  prprelprb  47511  reuprpr  47517  isgbe  47745  isgbow  47746  isgbo  47747  sbgoldbalt  47775  sgoldbeven3prm  47777  mogoldbb  47779  sbgoldbo  47781  nnsum3primesle9  47788  usgrgrtrirex  47942  grlimgrtri  47988  bigoval  48531  elbigo  48533  iscnrm3r  48929  iscnrm3l  48932