Theorem 2rexbidv 3228

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  f1oiso  7387  elrnmpog  7585  elrnmpo  7586  ralrnmpo  7589  ovelrn  7626  opiota  8100  omeu  8641  oeeui  8658  eroveu  8870  erov  8872  elfiun  9499  dffi3  9500  xpwdomg  9654  brdom7disj  10600  brdom6disj  10601  genpv  11068  genpelv  11069  axcnre  11233  supadd  12263  supmullem1  12265  supmullem2  12266  supmul  12267  01sqrexlem6  15296  ello1  15561  ello1mpt  15567  elo1  15572  lo1o1  15578  o1lo1  15583  bezoutlem1  16586  bezoutlem3  16588  bezoutlem4  16589  bezout  16590  pythagtriplem2  16864  pythagtriplem19  16880  pythagtrip  16881  pcval  16891  pceu  16893  pczpre  16894  pcdiv  16899  4sqlem2  16996  4sqlem3  16997  4sqlem4  16999  4sq  17011  vdwlem1  17028  vdwlem12  17039  vdwlem13  17040  vdwnnlem1  17042  vdwnnlem2  17043  vdwnnlem3  17044  vdwnn  17045  ramub2  17061  rami  17062  cat1lem  18163  cat1  18164  pgpfac1lem3  20121  lspprel  21116  znunit  21605  cayleyhamiltonALT  22918  hausnei  23357  isreg2  23406  txuni2  23594  txbas  23596  xkoopn  23618  txcls  23633  txcnpi  23637  txdis1cn  23664  txtube  23669  txcmplem1  23670  hausdiag  23674  tx1stc  23679  regr1lem2  23769  qustgplem  24150  met2ndci  24556  dyadmax  25652  i1fadd  25749  i1fmul  25750  elply  26254  2sqlem2  27480  2sqlem8  27488  2sqlem9  27489  2sqlem11  27491  elmade  27924  mulsval  28153  mulsval2lem  28154  mulsproplem9  28168  mulsproplem12  28171  ssltmul1  28191  ssltmul2  28192  mulsuniflem  28193  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  mulsunif2  28214  precsexlemcbv  28248  precsexlem9  28257  precsexlem11  28259  elzs12  28439  remulscllem1  28450  istrkgld  28485  istrkg3ld  28487  axtgupdim2  28497  axtgeucl  28498  legov  28611  iscgra  28835  dfcgra2  28856  axsegconlem1  28950  axpasch  28974  axlowdim  28994  axeuclidlem  28995  nb3grpr  29417  upgr4cycl4dv4e  30217  vdgn1frgrv2  30328  fusgr2wsp2nb  30366  l2p  30511  br8d  32632  constrsuc  33728  constrsslem  33731  constrconj  33735  pstmval  33841  eulerpartlemgh  34343  eulerpartlemgs2  34345  cvmliftlem15  35266  cvmlift2lem10  35280  satf  35321  satfv0  35326  satfrnmapom  35338  satfv0fun  35339  satf0op  35345  sat1el2xp  35347  fmlafvel  35353  fmla1  35355  fmlaomn0  35358  gonan0  35360  goaln0  35361  gonar  35363  goalr  35365  fmlasucdisj  35367  satffunlem2lem1  35372  dmopab3rexdif  35373  satfv0fvfmla0  35381  sategoelfvb  35387  satfv1fvfmla1  35391  2goelgoanfmla1  35392  br8  35718  br6  35719  br4  35720  elaltxp  35939  brsegle  36072  ellines  36116  nn0prpwlem  36288  nn0prpw  36289  ptrest  37579  ismblfin  37621  itg2addnclem3  37633  itg2addnc  37634  releldmqscoss  38616  isline  39696  psubspi  39704  paddfval  39754  elpadd  39756  paddvaln0N  39758  3rspcedvd  42208  flt4lem7  42614  nna4b4nsq  42615  mzpcompact2lem  42707  mzpcompact2  42708  sbc4rexgOLD  42746  pell1qrval  42802  elpell1qr  42803  pell14qrval  42804  elpell14qr  42805  pell1234qrval  42806  elpell1234qr  42807  jm2.27  42965  expdiophlem1  42978  oenord1  43278  oaun3lem1  43336  clsk1independent  44008  limclner  45572  fourierdlem42  46070  fourierdlem48  46075  sprel  47358  prelspr  47360  prprelb  47390  prprelprb  47391  reuprpr  47397  isgbe  47625  isgbow  47626  isgbo  47627  sbgoldbalt  47655  sgoldbeven3prm  47657  mogoldbb  47659  sbgoldbo  47661  nnsum3primesle9  47668  usgrgrtrirex  47799  grlimgrtri  47820  bigoval  48283  elbigo  48285  iscnrm3r  48628  iscnrm3l  48631