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

Theorem 2rexbidv 3205
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 3200 . 2 (𝜑 → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
32rexbidv 3200 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-rex 3067
This theorem is referenced by:  f1oiso  6744  elrnmpt2g  6919  elrnmpt2  6920  ralrnmpt2  6922  ovelrn  6957  opiota  7378  omeu  7819  oeeui  7836  eroveu  7995  erov  7997  elfiun  8492  dffi3  8493  xpwdomg  8646  brdom7disj  9555  brdom6disj  9556  genpv  10023  genpelv  10024  axcnre  10187  supadd  11193  supmullem1  11195  supmullem2  11196  supmul  11197  sqrlem6  14196  ello1  14454  ello1mpt  14460  elo1  14465  lo1o1  14471  o1lo1  14476  bezoutlem1  15464  bezoutlem3  15466  bezoutlem4  15467  bezout  15468  pythagtriplem2  15729  pythagtriplem19  15745  pythagtrip  15746  pcval  15756  pceu  15758  pczpre  15759  pcdiv  15764  4sqlem2  15860  4sqlem3  15861  4sqlem4  15863  4sq  15875  vdwlem1  15892  vdwlem12  15903  vdwlem13  15904  vdwnnlem1  15906  vdwnnlem2  15907  vdwnnlem3  15908  vdwnn  15909  ramub2  15925  rami  15926  pgpfac1lem3  18684  lspprel  19307  znunit  20127  cayleyhamiltonALT  20916  hausnei  21353  isreg2  21402  txuni2  21589  txbas  21591  xkoopn  21613  txcls  21628  txcnpi  21632  txdis1cn  21659  txtube  21664  txcmplem1  21665  hausdiag  21669  tx1stc  21674  regr1lem2  21764  qustgplem  22144  met2ndci  22547  dyadmax  23586  i1fadd  23682  i1fmul  23683  elply  24171  2sqlem2  25364  2sqlem8  25372  2sqlem9  25373  2sqlem11  25375  istrkgld  25579  axtgeucl  25592  legov  25701  iscgra  25922  dfcgra2  25942  axsegconlem1  26018  axpasch  26042  axlowdim  26062  axeuclidlem  26063  nb3grpr  26507  upgr4cycl4dv4e  27365  vdgn1frgrv2  27478  fusgr2wsp2nb  27516  l2p  27673  br8d  29760  pstmval  30278  eulerpartlemgh  30780  eulerpartlemgs2  30782  cvmliftlem15  31618  cvmlift2lem10  31632  br8  31984  br6  31985  br4  31986  elaltxp  32419  brsegle  32552  ellines  32596  nn0prpwlem  32654  nn0prpw  32655  ptrest  33741  ismblfin  33783  itg2addnclem3  33795  itg2addnc  33796  isline  35547  psubspi  35555  paddfval  35605  elpadd  35607  paddvaln0N  35609  mzpcompact2lem  37840  mzpcompact2  37841  sbc4rexgOLD  37880  pell1qrval  37936  elpell1qr  37937  pell14qrval  37938  elpell14qr  37939  pell1234qrval  37940  elpell1234qr  37941  jm2.27  38101  expdiophlem1  38114  clsk1independent  38870  limclner  40401  fourierdlem42  40883  fourierdlem48  40888  isgbe  42167  isgbow  42168  isgbo  42169  sbgoldbalt  42197  sgoldbeven3prm  42199  mogoldbb  42201  sbgoldbo  42203  nnsum3primesle9  42210  sprel  42262  prelspr  42264  bigoval  42871  elbigo  42873
  Copyright terms: Public domain W3C validator