Theorem 2rexbidv 3259

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

Syntax hints:   → wi 4   ↔ wb 209  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  f1oiso  7083  elrnmpog  7265  elrnmpo  7266  ralrnmpo  7268  ovelrn  7304  opiota  7739  omeu  8194  oeeui  8211  eroveu  8375  erov  8377  elfiun  8878  dffi3  8879  xpwdomg  9033  brdom7disj  9942  brdom6disj  9943  genpv  10410  genpelv  10411  axcnre  10575  supadd  11596  supmullem1  11598  supmullem2  11599  supmul  11600  sqrlem6  14599  ello1  14864  ello1mpt  14870  elo1  14875  lo1o1  14881  o1lo1  14886  bezoutlem1  15877  bezoutlem3  15879  bezoutlem4  15880  bezout  15881  pythagtriplem2  16144  pythagtriplem19  16160  pythagtrip  16161  pcval  16171  pceu  16173  pczpre  16174  pcdiv  16179  4sqlem2  16275  4sqlem3  16276  4sqlem4  16278  4sq  16290  vdwlem1  16307  vdwlem12  16318  vdwlem13  16319  vdwnnlem1  16321  vdwnnlem2  16322  vdwnnlem3  16323  vdwnn  16324  ramub2  16340  rami  16341  pgpfac1lem3  19192  lspprel  19859  znunit  20255  cayleyhamiltonALT  21496  hausnei  21933  isreg2  21982  txuni2  22170  txbas  22172  xkoopn  22194  txcls  22209  txcnpi  22213  txdis1cn  22240  txtube  22245  txcmplem1  22246  hausdiag  22250  tx1stc  22255  regr1lem2  22345  qustgplem  22726  met2ndci  23129  dyadmax  24202  i1fadd  24299  i1fmul  24300  elply  24792  2sqlem2  26002  2sqlem8  26010  2sqlem9  26011  2sqlem11  26013  istrkgld  26253  istrkg3ld  26255  axtgupdim2  26265  axtgeucl  26266  legov  26379  iscgra  26603  dfcgra2  26624  axsegconlem1  26711  axpasch  26735  axlowdim  26755  axeuclidlem  26756  nb3grpr  27172  upgr4cycl4dv4e  27970  vdgn1frgrv2  28081  fusgr2wsp2nb  28119  l2p  28262  br8d  30374  pstmval  31248  eulerpartlemgh  31746  eulerpartlemgs2  31748  cvmliftlem15  32658  cvmlift2lem10  32672  satf  32713  satfv0  32718  satfrnmapom  32730  satfv0fun  32731  satf0op  32737  sat1el2xp  32739  fmlafvel  32745  fmla1  32747  fmlaomn0  32750  gonan0  32752  goaln0  32753  gonar  32755  goalr  32757  fmlasucdisj  32759  satffunlem2lem1  32764  dmopab3rexdif  32765  satfv0fvfmla0  32773  sategoelfvb  32779  satfv1fvfmla1  32783  2goelgoanfmla1  32784  br8  33105  br6  33106  br4  33107  elaltxp  33549  brsegle  33682  ellines  33726  nn0prpwlem  33783  nn0prpw  33784  ptrest  35056  ismblfin  35098  itg2addnclem3  35110  itg2addnc  35111  releldmqscoss  36054  isline  37035  psubspi  37043  paddfval  37093  elpadd  37095  paddvaln0N  37097  3rspcedvd  39397  mzpcompact2lem  39692  mzpcompact2  39693  sbc4rexgOLD  39731  pell1qrval  39787  elpell1qr  39788  pell14qrval  39789  elpell14qr  39790  pell1234qrval  39791  elpell1234qr  39792  jm2.27  39949  expdiophlem1  39962  clsk1independent  40749  limclner  42293  fourierdlem42  42791  fourierdlem48  42796  sprel  44001  prelspr  44003  prprelb  44033  prprelprb  44034  reuprpr  44040  isgbe  44269  isgbow  44270  isgbo  44271  sbgoldbalt  44299  sgoldbeven3prm  44301  mogoldbb  44303  sbgoldbo  44305  nnsum3primesle9  44312  bigoval  44963  elbigo  44965