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

Theorem 2rexbidv 3292
Description: Formula-building rule for restricted existential quantifiers (deduction form). (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 3289 . 2 (𝜑 → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
32rexbidv 3289 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wrex 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3138
This theorem is referenced by:  f1oiso  7086  elrnmpog  7268  elrnmpo  7269  ralrnmpo  7271  ovelrn  7307  opiota  7740  omeu  8194  oeeui  8211  eroveu  8375  erov  8377  elfiun  8878  dffi3  8879  xpwdomg  9033  brdom7disj  9938  brdom6disj  9939  genpv  10406  genpelv  10407  axcnre  10571  supadd  11594  supmullem1  11596  supmullem2  11597  supmul  11598  sqrlem6  14596  ello1  14861  ello1mpt  14867  elo1  14872  lo1o1  14878  o1lo1  14883  bezoutlem1  15874  bezoutlem3  15876  bezoutlem4  15877  bezout  15878  pythagtriplem2  16141  pythagtriplem19  16157  pythagtrip  16158  pcval  16168  pceu  16170  pczpre  16171  pcdiv  16176  4sqlem2  16272  4sqlem3  16273  4sqlem4  16275  4sq  16287  vdwlem1  16304  vdwlem12  16315  vdwlem13  16316  vdwnnlem1  16318  vdwnnlem2  16319  vdwnnlem3  16320  vdwnn  16321  ramub2  16337  rami  16338  pgpfac1lem3  19188  lspprel  19852  znunit  20696  cayleyhamiltonALT  21485  hausnei  21922  isreg2  21971  txuni2  22159  txbas  22161  xkoopn  22183  txcls  22198  txcnpi  22202  txdis1cn  22229  txtube  22234  txcmplem1  22235  hausdiag  22239  tx1stc  22244  regr1lem2  22334  qustgplem  22715  met2ndci  23118  dyadmax  24191  i1fadd  24288  i1fmul  24289  elply  24781  2sqlem2  25991  2sqlem8  25999  2sqlem9  26000  2sqlem11  26002  istrkgld  26242  istrkg3ld  26244  axtgupdim2  26254  axtgeucl  26255  legov  26368  iscgra  26592  dfcgra2  26613  axsegconlem1  26700  axpasch  26724  axlowdim  26744  axeuclidlem  26745  nb3grpr  27161  upgr4cycl4dv4e  27959  vdgn1frgrv2  28070  fusgr2wsp2nb  28108  l2p  28251  br8d  30358  pstmval  31156  eulerpartlemgh  31654  eulerpartlemgs2  31656  cvmliftlem15  32563  cvmlift2lem10  32577  satf  32618  satfv0  32623  satfrnmapom  32635  satfv0fun  32636  satf0op  32642  sat1el2xp  32644  fmlafvel  32650  fmla1  32652  fmlaomn0  32655  gonan0  32657  goaln0  32658  gonar  32660  goalr  32662  fmlasucdisj  32664  satffunlem2lem1  32669  dmopab3rexdif  32670  satfv0fvfmla0  32678  sategoelfvb  32684  satfv1fvfmla1  32688  2goelgoanfmla1  32689  br8  33010  br6  33011  br4  33012  elaltxp  33454  brsegle  33587  ellines  33631  nn0prpwlem  33688  nn0prpw  33689  ptrest  34956  ismblfin  34998  itg2addnclem3  35010  itg2addnc  35011  releldmqscoss  35954  isline  36935  psubspi  36943  paddfval  36993  elpadd  36995  paddvaln0N  36997  3rspcedvd  39256  mzpcompact2lem  39524  mzpcompact2  39525  sbc4rexgOLD  39563  pell1qrval  39619  elpell1qr  39620  pell14qrval  39621  elpell14qr  39622  pell1234qrval  39623  elpell1234qr  39624  jm2.27  39781  expdiophlem1  39794  clsk1independent  40584  limclner  42135  fourierdlem42  42633  fourierdlem48  42638  sprel  43843  prelspr  43845  prprelb  43875  prprelprb  43876  reuprpr  43882  isgbe  44111  isgbow  44112  isgbo  44113  sbgoldbalt  44141  sgoldbeven3prm  44143  mogoldbb  44145  sbgoldbo  44147  nnsum3primesle9  44154  bigoval  44804  elbigo  44806
  Copyright terms: Public domain W3C validator