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

Theorem 2rexbidv 3050
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 3045 . 2 (𝜑 → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
32rexbidv 3045 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-rex 2913
This theorem is referenced by:  f1oiso  6555  elrnmpt2g  6725  elrnmpt2  6726  ralrnmpt2  6728  ovelrn  6763  opiota  7174  omeu  7610  oeeui  7627  eroveu  7787  erov  7789  elfiun  8280  dffi3  8281  xpwdomg  8434  brdom7disj  9297  brdom6disj  9298  genpv  9765  genpelv  9766  axcnre  9929  supadd  10935  supmullem1  10937  supmullem2  10938  supmul  10939  sqrlem6  13922  ello1  14180  ello1mpt  14186  elo1  14191  lo1o1  14197  o1lo1  14202  bezoutlem1  15180  bezoutlem3  15182  bezoutlem4  15183  bezout  15184  pythagtriplem2  15446  pythagtriplem19  15462  pythagtrip  15463  pcval  15473  pceu  15475  pczpre  15476  pcdiv  15481  4sqlem2  15577  4sqlem3  15578  4sqlem4  15580  4sq  15592  vdwlem1  15609  vdwlem12  15620  vdwlem13  15621  vdwnnlem1  15623  vdwnnlem2  15624  vdwnnlem3  15625  vdwnn  15626  ramub2  15642  rami  15643  pgpfac1lem3  18397  lspprel  19013  znunit  19831  cayleyhamiltonALT  20615  hausnei  21042  isreg2  21091  txuni2  21278  txbas  21280  xkoopn  21302  txcls  21317  txcnpi  21321  txdis1cn  21348  txtube  21353  txcmplem1  21354  hausdiag  21358  tx1stc  21363  regr1lem2  21453  qustgplem  21834  met2ndci  22237  dyadmax  23272  i1fadd  23368  i1fmul  23369  elply  23855  2sqlem2  25043  2sqlem8  25051  2sqlem9  25052  2sqlem11  25054  istrkgld  25258  axtgeucl  25271  legov  25380  iscgra  25601  dfcgra2  25621  axsegconlem1  25697  axpasch  25721  axlowdim  25741  axeuclidlem  25742  nb3grpr  26171  upgr4cycl4dv4e  26911  vdgn1frgrv2  27024  fusgr2wsp2nb  27056  l2p  27184  br8d  29265  pstmval  29720  eulerpartlemgh  30221  eulerpartlemgs2  30223  cvmliftlem15  30988  cvmlift2lem10  31002  br8  31354  br6  31355  br4  31356  elaltxp  31724  brsegle  31857  ellines  31901  nn0prpwlem  31959  nn0prpw  31960  ptrest  33040  ismblfin  33082  itg2addnclem3  33095  itg2addnc  33096  isline  34505  psubspi  34513  paddfval  34563  elpadd  34565  paddvaln0N  34567  mzpcompact2lem  36794  mzpcompact2  36795  sbc4rexgOLD  36834  pell1qrval  36890  elpell1qr  36891  pell14qrval  36892  elpell14qr  36893  pell1234qrval  36894  elpell1234qr  36895  jm2.27  37055  expdiophlem1  37068  clsk1independent  37826  limclner  39287  fourierdlem42  39673  fourierdlem48  39678  isgbe  40934  isgbo  40935  isgboa  40936  sgoldbalt  40964  nnsum3primesle9  40971  sprel  41022  prelspr  41024  bigoval  41635  elbigo  41637
  Copyright terms: Public domain W3C validator