Theorem 2rexbidv 3209

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3060

This theorem is referenced by:  f1oiso  7358  elrnmpog  7556  elrnmpo  7557  ralrnmpo  7560  ovelrn  7597  opiota  8064  omeu  8606  oeeui  8623  eroveu  8831  erov  8833  elfiun  9455  dffi3  9456  xpwdomg  9610  brdom7disj  10556  brdom6disj  10557  genpv  11024  genpelv  11025  axcnre  11189  supadd  12215  supmullem1  12217  supmullem2  12218  supmul  12219  01sqrexlem6  15230  ello1  15495  ello1mpt  15501  elo1  15506  lo1o1  15512  o1lo1  15517  bezoutlem1  16518  bezoutlem3  16520  bezoutlem4  16521  bezout  16522  pythagtriplem2  16789  pythagtriplem19  16805  pythagtrip  16806  pcval  16816  pceu  16818  pczpre  16819  pcdiv  16824  4sqlem2  16921  4sqlem3  16922  4sqlem4  16924  4sq  16936  vdwlem1  16953  vdwlem12  16964  vdwlem13  16965  vdwnnlem1  16967  vdwnnlem2  16968  vdwnnlem3  16969  vdwnn  16970  ramub2  16986  rami  16987  cat1lem  18088  cat1  18089  pgpfac1lem3  20046  lspprel  20991  znunit  21514  cayleyhamiltonALT  22837  hausnei  23276  isreg2  23325  txuni2  23513  txbas  23515  xkoopn  23537  txcls  23552  txcnpi  23556  txdis1cn  23583  txtube  23588  txcmplem1  23589  hausdiag  23593  tx1stc  23598  regr1lem2  23688  qustgplem  24069  met2ndci  24475  dyadmax  25571  i1fadd  25668  i1fmul  25669  elply  26174  2sqlem2  27396  2sqlem8  27404  2sqlem9  27405  2sqlem11  27407  elmade  27840  mulsval  28059  mulsval2lem  28060  mulsproplem9  28074  mulsproplem12  28077  ssltmul1  28097  ssltmul2  28098  mulsuniflem  28099  addsdilem2  28102  mulsasslem1  28113  mulsasslem2  28114  mulsunif2  28120  precsexlemcbv  28154  precsexlem9  28163  precsexlem11  28165  remulscllem1  28300  istrkgld  28335  istrkg3ld  28337  axtgupdim2  28347  axtgeucl  28348  legov  28461  iscgra  28685  dfcgra2  28706  axsegconlem1  28800  axpasch  28824  axlowdim  28844  axeuclidlem  28845  nb3grpr  29267  upgr4cycl4dv4e  30067  vdgn1frgrv2  30178  fusgr2wsp2nb  30216  l2p  30361  br8d  32479  pstmval  33627  eulerpartlemgh  34129  eulerpartlemgs2  34131  cvmliftlem15  35039  cvmlift2lem10  35053  satf  35094  satfv0  35099  satfrnmapom  35111  satfv0fun  35112  satf0op  35118  sat1el2xp  35120  fmlafvel  35126  fmla1  35128  fmlaomn0  35131  gonan0  35133  goaln0  35134  gonar  35136  goalr  35138  fmlasucdisj  35140  satffunlem2lem1  35145  dmopab3rexdif  35146  satfv0fvfmla0  35154  sategoelfvb  35160  satfv1fvfmla1  35164  2goelgoanfmla1  35165  br8  35481  br6  35482  br4  35483  elaltxp  35702  brsegle  35835  ellines  35879  nn0prpwlem  35937  nn0prpw  35938  ptrest  37223  ismblfin  37265  itg2addnclem3  37277  itg2addnc  37278  releldmqscoss  38262  isline  39342  psubspi  39350  paddfval  39400  elpadd  39402  paddvaln0N  39404  3rspcedvd  41837  flt4lem7  42218  nna4b4nsq  42219  mzpcompact2lem  42313  mzpcompact2  42314  sbc4rexgOLD  42352  pell1qrval  42408  elpell1qr  42409  pell14qrval  42410  elpell14qr  42411  pell1234qrval  42412  elpell1234qr  42413  jm2.27  42571  expdiophlem1  42584  oenord1  42887  oaun3lem1  42945  clsk1independent  43618  limclner  45177  fourierdlem42  45675  fourierdlem48  45680  sprel  46961  prelspr  46963  prprelb  46993  prprelprb  46994  reuprpr  47000  isgbe  47228  isgbow  47229  isgbo  47230  sbgoldbalt  47258  sgoldbeven3prm  47260  mogoldbb  47262  sbgoldbo  47264  nnsum3primesle9  47271  bigoval  47808  elbigo  47810  iscnrm3r  48153  iscnrm3l  48156