Theorem 2rexbidv 3213

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3074

This theorem is referenced by:  f1oiso  7296  elrnmpog  7491  elrnmpo  7492  ralrnmpo  7494  ovelrn  7530  opiota  7991  omeu  8532  oeeui  8549  eroveu  8751  erov  8753  elfiun  9366  dffi3  9367  xpwdomg  9521  brdom7disj  10467  brdom6disj  10468  genpv  10935  genpelv  10936  axcnre  11100  supadd  12123  supmullem1  12125  supmullem2  12126  supmul  12127  01sqrexlem6  15132  ello1  15397  ello1mpt  15403  elo1  15408  lo1o1  15414  o1lo1  15419  bezoutlem1  16420  bezoutlem3  16422  bezoutlem4  16423  bezout  16424  pythagtriplem2  16689  pythagtriplem19  16705  pythagtrip  16706  pcval  16716  pceu  16718  pczpre  16719  pcdiv  16724  4sqlem2  16821  4sqlem3  16822  4sqlem4  16824  4sq  16836  vdwlem1  16853  vdwlem12  16864  vdwlem13  16865  vdwnnlem1  16867  vdwnnlem2  16868  vdwnnlem3  16869  vdwnn  16870  ramub2  16886  rami  16887  cat1lem  17982  cat1  17983  pgpfac1lem3  19856  lspprel  20555  znunit  20970  cayleyhamiltonALT  22240  hausnei  22679  isreg2  22728  txuni2  22916  txbas  22918  xkoopn  22940  txcls  22955  txcnpi  22959  txdis1cn  22986  txtube  22991  txcmplem1  22992  hausdiag  22996  tx1stc  23001  regr1lem2  23091  qustgplem  23472  met2ndci  23878  dyadmax  24962  i1fadd  25059  i1fmul  25060  elply  25556  2sqlem2  26766  2sqlem8  26774  2sqlem9  26775  2sqlem11  26777  elmade  27197  istrkgld  27401  istrkg3ld  27403  axtgupdim2  27413  axtgeucl  27414  legov  27527  iscgra  27751  dfcgra2  27772  axsegconlem1  27866  axpasch  27890  axlowdim  27910  axeuclidlem  27911  nb3grpr  28330  upgr4cycl4dv4e  29129  vdgn1frgrv2  29240  fusgr2wsp2nb  29278  l2p  29421  br8d  31529  pstmval  32476  eulerpartlemgh  32978  eulerpartlemgs2  32980  cvmliftlem15  33892  cvmlift2lem10  33906  satf  33947  satfv0  33952  satfrnmapom  33964  satfv0fun  33965  satf0op  33971  sat1el2xp  33973  fmlafvel  33979  fmla1  33981  fmlaomn0  33984  gonan0  33986  goaln0  33987  gonar  33989  goalr  33991  fmlasucdisj  33993  satffunlem2lem1  33998  dmopab3rexdif  33999  satfv0fvfmla0  34007  sategoelfvb  34013  satfv1fvfmla1  34017  2goelgoanfmla1  34018  br8  34329  br6  34330  br4  34331  mulsval  34408  elaltxp  34560  brsegle  34693  ellines  34737  nn0prpwlem  34794  nn0prpw  34795  ptrest  36077  ismblfin  36119  itg2addnclem3  36131  itg2addnc  36132  releldmqscoss  37122  isline  38202  psubspi  38210  paddfval  38260  elpadd  38262  paddvaln0N  38264  3rspcedvd  40634  flt4lem7  40983  nna4b4nsq  40984  mzpcompact2lem  41060  mzpcompact2  41061  sbc4rexgOLD  41099  pell1qrval  41155  elpell1qr  41156  pell14qrval  41157  elpell14qr  41158  pell1234qrval  41159  elpell1234qr  41160  jm2.27  41318  expdiophlem1  41331  oenord1  41636  clsk1independent  42308  limclner  43882  fourierdlem42  44380  fourierdlem48  44385  sprel  45666  prelspr  45668  prprelb  45698  prprelprb  45699  reuprpr  45705  isgbe  45933  isgbow  45934  isgbo  45935  sbgoldbalt  45963  sgoldbeven3prm  45965  mogoldbb  45967  sbgoldbo  45969  nnsum3primesle9  45976  bigoval  46625  elbigo  46627  iscnrm3r  46971  iscnrm3l  46974