Theorem 2rexbidv 3217

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

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

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  f1oiso  7350  elrnmpog  7546  elrnmpo  7547  ralrnmpo  7549  ovelrn  7585  opiota  8047  omeu  8587  oeeui  8604  eroveu  8808  erov  8810  elfiun  9427  dffi3  9428  xpwdomg  9582  brdom7disj  10528  brdom6disj  10529  genpv  10996  genpelv  10997  axcnre  11161  supadd  12186  supmullem1  12188  supmullem2  12189  supmul  12190  01sqrexlem6  15198  ello1  15463  ello1mpt  15469  elo1  15474  lo1o1  15480  o1lo1  15485  bezoutlem1  16485  bezoutlem3  16487  bezoutlem4  16488  bezout  16489  pythagtriplem2  16754  pythagtriplem19  16770  pythagtrip  16771  pcval  16781  pceu  16783  pczpre  16784  pcdiv  16789  4sqlem2  16886  4sqlem3  16887  4sqlem4  16889  4sq  16901  vdwlem1  16918  vdwlem12  16929  vdwlem13  16930  vdwnnlem1  16932  vdwnnlem2  16933  vdwnnlem3  16934  vdwnn  16935  ramub2  16951  rami  16952  cat1lem  18050  cat1  18051  pgpfac1lem3  19988  lspprel  20849  znunit  21338  cayleyhamiltonALT  22613  hausnei  23052  isreg2  23101  txuni2  23289  txbas  23291  xkoopn  23313  txcls  23328  txcnpi  23332  txdis1cn  23359  txtube  23364  txcmplem1  23365  hausdiag  23369  tx1stc  23374  regr1lem2  23464  qustgplem  23845  met2ndci  24251  dyadmax  25347  i1fadd  25444  i1fmul  25445  elply  25944  2sqlem2  27157  2sqlem8  27165  2sqlem9  27166  2sqlem11  27168  elmade  27599  mulsval  27804  mulsval2lem  27805  mulsproplem9  27819  mulsproplem12  27822  ssltmul1  27841  ssltmul2  27842  mulsuniflem  27843  addsdilem2  27846  mulsasslem1  27857  mulsasslem2  27858  precsexlemcbv  27891  precsexlem9  27900  precsexlem11  27902  istrkgld  27977  istrkg3ld  27979  axtgupdim2  27989  axtgeucl  27990  legov  28103  iscgra  28327  dfcgra2  28348  axsegconlem1  28442  axpasch  28466  axlowdim  28486  axeuclidlem  28487  nb3grpr  28906  upgr4cycl4dv4e  29705  vdgn1frgrv2  29816  fusgr2wsp2nb  29854  l2p  29999  br8d  32106  pstmval  33173  eulerpartlemgh  33675  eulerpartlemgs2  33677  cvmliftlem15  34587  cvmlift2lem10  34601  satf  34642  satfv0  34647  satfrnmapom  34659  satfv0fun  34660  satf0op  34666  sat1el2xp  34668  fmlafvel  34674  fmla1  34676  fmlaomn0  34679  gonan0  34681  goaln0  34682  gonar  34684  goalr  34686  fmlasucdisj  34688  satffunlem2lem1  34693  dmopab3rexdif  34694  satfv0fvfmla0  34702  sategoelfvb  34708  satfv1fvfmla1  34712  2goelgoanfmla1  34713  br8  35030  br6  35031  br4  35032  elaltxp  35251  brsegle  35384  ellines  35428  nn0prpwlem  35510  nn0prpw  35511  ptrest  36790  ismblfin  36832  itg2addnclem3  36844  itg2addnc  36845  releldmqscoss  37833  isline  38913  psubspi  38921  paddfval  38971  elpadd  38973  paddvaln0N  38975  3rspcedvd  41337  flt4lem7  41703  nna4b4nsq  41704  mzpcompact2lem  41791  mzpcompact2  41792  sbc4rexgOLD  41830  pell1qrval  41886  elpell1qr  41887  pell14qrval  41888  elpell14qr  41889  pell1234qrval  41890  elpell1234qr  41891  jm2.27  42049  expdiophlem1  42062  oenord1  42368  oaun3lem1  42426  clsk1independent  43099  limclner  44665  fourierdlem42  45163  fourierdlem48  45168  sprel  46450  prelspr  46452  prprelb  46482  prprelprb  46483  reuprpr  46489  isgbe  46717  isgbow  46718  isgbo  46719  sbgoldbalt  46747  sgoldbeven3prm  46749  mogoldbb  46751  sbgoldbo  46753  nnsum3primesle9  46760  bigoval  47322  elbigo  47324  iscnrm3r  47668  iscnrm3l  47671