Theorem 2rexbidv 3203

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

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

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 3055

This theorem is referenced by:  f1oiso  7329  elrnmpog  7527  elrnmpo  7528  ralrnmpo  7531  ovelrn  7568  opiota  8041  omeu  8552  oeeui  8569  eroveu  8788  erov  8790  elfiun  9388  dffi3  9389  xpwdomg  9545  brdom7disj  10491  brdom6disj  10492  genpv  10959  genpelv  10960  axcnre  11124  supadd  12158  supmullem1  12160  supmullem2  12161  supmul  12162  01sqrexlem6  15220  ello1  15488  ello1mpt  15494  elo1  15499  lo1o1  15505  o1lo1  15510  bezoutlem1  16516  bezoutlem3  16518  bezoutlem4  16519  bezout  16520  pythagtriplem2  16795  pythagtriplem19  16811  pythagtrip  16812  pcval  16822  pceu  16824  pczpre  16825  pcdiv  16830  4sqlem2  16927  4sqlem3  16928  4sqlem4  16930  4sq  16942  vdwlem1  16959  vdwlem12  16970  vdwlem13  16971  vdwnnlem1  16973  vdwnnlem2  16974  vdwnnlem3  16975  vdwnn  16976  ramub2  16992  rami  16993  cat1lem  18065  cat1  18066  pgpfac1lem3  20016  lspprel  21008  znunit  21480  cayleyhamiltonALT  22785  hausnei  23222  isreg2  23271  txuni2  23459  txbas  23461  xkoopn  23483  txcls  23498  txcnpi  23502  txdis1cn  23529  txtube  23534  txcmplem1  23535  hausdiag  23539  tx1stc  23544  regr1lem2  23634  qustgplem  24015  met2ndci  24417  dyadmax  25506  i1fadd  25603  i1fmul  25604  elply  26107  2sqlem2  27336  2sqlem8  27344  2sqlem9  27345  2sqlem11  27347  elmade  27786  mulsval  28019  mulsval2lem  28020  mulsproplem9  28034  mulsproplem12  28037  ssltmul1  28057  ssltmul2  28058  mulsuniflem  28059  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  mulsunif2  28080  precsexlemcbv  28115  precsexlem9  28124  precsexlem11  28126  eucliddivs  28272  elzs12  28344  zs12ge0  28349  remulscllem1  28358  istrkgld  28393  istrkg3ld  28395  axtgupdim2  28405  axtgeucl  28406  legov  28519  iscgra  28743  dfcgra2  28764  axsegconlem1  28851  axpasch  28875  axlowdim  28895  axeuclidlem  28896  nb3grpr  29316  upgr4cycl4dv4e  30121  vdgn1frgrv2  30232  fusgr2wsp2nb  30270  l2p  30415  br8d  32545  gsumwun  33012  constrsuc  33735  constrsslem  33738  constrconj  33742  constrllcllem  33749  constrlccllem  33750  constrcccllem  33751  constrcbvlem  33752  pstmval  33892  eulerpartlemgh  34376  eulerpartlemgs2  34378  cvmliftlem15  35292  cvmlift2lem10  35306  satf  35347  satfv0  35352  satfrnmapom  35364  satfv0fun  35365  satf0op  35371  sat1el2xp  35373  fmlafvel  35379  fmla1  35381  fmlaomn0  35384  gonan0  35386  goaln0  35387  gonar  35389  goalr  35391  fmlasucdisj  35393  satffunlem2lem1  35398  dmopab3rexdif  35399  satfv0fvfmla0  35407  sategoelfvb  35413  satfv1fvfmla1  35417  2goelgoanfmla1  35418  br8  35750  br6  35751  br4  35752  elaltxp  35970  brsegle  36103  ellines  36147  nn0prpwlem  36317  nn0prpw  36318  ptrest  37620  ismblfin  37662  itg2addnclem3  37674  itg2addnc  37675  releldmqscoss  38659  isline  39740  psubspi  39748  paddfval  39798  elpadd  39800  paddvaln0N  39802  3rspcedvd  42210  flt4lem7  42654  nna4b4nsq  42655  mzpcompact2lem  42746  mzpcompact2  42747  sbc4rexgOLD  42785  pell1qrval  42841  elpell1qr  42842  pell14qrval  42843  elpell14qr  42844  pell1234qrval  42845  elpell1234qr  42846  jm2.27  43004  expdiophlem1  43017  oenord1  43312  oaun3lem1  43370  clsk1independent  44042  limclner  45656  fourierdlem42  46154  fourierdlem48  46159  sprel  47489  prelspr  47491  prprelb  47521  prprelprb  47522  reuprpr  47528  isgbe  47756  isgbow  47757  isgbo  47758  sbgoldbalt  47786  sgoldbeven3prm  47788  mogoldbb  47790  sbgoldbo  47792  nnsum3primesle9  47799  usgrgrtrirex  47953  grlimgrtri  47999  bigoval  48542  elbigo  48544  iscnrm3r  48940  iscnrm3l  48943