MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2rexbidv Structured version   Visualization version   GIF version

Theorem 2rexbidv 3086
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (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
StepHypRef Expression
1 2rexbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21rexbidv 3081 . 2 (𝜑 → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
32rexbidv 3081 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947
This theorem is referenced by:  f1oiso  6641  elrnmpt2g  6814  elrnmpt2  6815  ralrnmpt2  6817  ovelrn  6852  opiota  7273  omeu  7710  oeeui  7727  eroveu  7885  erov  7887  elfiun  8377  dffi3  8378  xpwdomg  8531  brdom7disj  9391  brdom6disj  9392  genpv  9859  genpelv  9860  axcnre  10023  supadd  11029  supmullem1  11031  supmullem2  11032  supmul  11033  sqrlem6  14032  ello1  14290  ello1mpt  14296  elo1  14301  lo1o1  14307  o1lo1  14312  bezoutlem1  15303  bezoutlem3  15305  bezoutlem4  15306  bezout  15307  pythagtriplem2  15569  pythagtriplem19  15585  pythagtrip  15586  pcval  15596  pceu  15598  pczpre  15599  pcdiv  15604  4sqlem2  15700  4sqlem3  15701  4sqlem4  15703  4sq  15715  vdwlem1  15732  vdwlem12  15743  vdwlem13  15744  vdwnnlem1  15746  vdwnnlem2  15747  vdwnnlem3  15748  vdwnn  15749  ramub2  15765  rami  15766  pgpfac1lem3  18522  lspprel  19142  znunit  19960  cayleyhamiltonALT  20744  hausnei  21180  isreg2  21229  txuni2  21416  txbas  21418  xkoopn  21440  txcls  21455  txcnpi  21459  txdis1cn  21486  txtube  21491  txcmplem1  21492  hausdiag  21496  tx1stc  21501  regr1lem2  21591  qustgplem  21971  met2ndci  22374  dyadmax  23412  i1fadd  23507  i1fmul  23508  elply  23996  2sqlem2  25188  2sqlem8  25196  2sqlem9  25197  2sqlem11  25199  istrkgld  25403  axtgeucl  25416  legov  25525  iscgra  25746  dfcgra2  25766  axsegconlem1  25842  axpasch  25866  axlowdim  25886  axeuclidlem  25887  nb3grpr  26328  upgr4cycl4dv4e  27163  vdgn1frgrv2  27276  fusgr2wsp2nb  27314  l2p  27461  br8d  29548  pstmval  30066  eulerpartlemgh  30568  eulerpartlemgs2  30570  cvmliftlem15  31406  cvmlift2lem10  31420  br8  31772  br6  31773  br4  31774  elaltxp  32207  brsegle  32340  ellines  32384  nn0prpwlem  32442  nn0prpw  32443  ptrest  33538  ismblfin  33580  itg2addnclem3  33593  itg2addnc  33594  isline  35343  psubspi  35351  paddfval  35401  elpadd  35403  paddvaln0N  35405  mzpcompact2lem  37631  mzpcompact2  37632  sbc4rexgOLD  37671  pell1qrval  37727  elpell1qr  37728  pell14qrval  37729  elpell14qr  37730  pell1234qrval  37731  elpell1234qr  37732  jm2.27  37892  expdiophlem1  37905  clsk1independent  38661  limclner  40201  fourierdlem42  40684  fourierdlem48  40689  isgbe  41964  isgbow  41965  isgbo  41966  sbgoldbalt  41994  sgoldbeven3prm  41996  mogoldbb  41998  sbgoldbo  42000  nnsum3primesle9  42007  sprel  42059  prelspr  42061  bigoval  42668  elbigo  42670
  Copyright terms: Public domain W3C validator