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

Theorem reximdv2 3158
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.)
Hypothesis
Ref Expression
reximdv2.1 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
Assertion
Ref Expression
reximdv2 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐵 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem reximdv2
StepHypRef Expression
1 reximdv2.1 . . 3 (𝜑 → ((𝑥𝐴𝜓) → (𝑥𝐵𝜒)))
21eximdv 1921 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) → ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3071 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3071 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 296 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1782  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-rex 3071
This theorem is referenced by:  reximdvai  3159  reximssdv  3166  ssrexv  4015  ssimaex  6930  nnsuc  7824  oaass  8512  omeulem1  8533  ssnnfi  9119  ssnnfiOLD  9120  findcard3  9235  findcard3OLD  9236  unfilem1  9260  epfrs  9675  alephval3  10054  isfin7-2  10340  fpwwe2lem12  10586  inawinalem  10633  ico0  13319  ioc0  13320  r19.2uz  15245  climrlim2  15438  prmdvdsncoprmbd  16610  iserodd  16715  ramub2  16894  prmgaplem6  16936  ablfaclem3  19874  unitgrp  20104  restnlly  22856  llyrest  22859  nllyrest  22860  llyidm  22862  nllyidm  22863  cnpflfi  23373  cnextcn  23441  ivthlem3  24840  dvfsumrlim  25418  lgsquadlem2  26752  oppperpex  27744  outpasch  27746  ushgredgedg  28226  ushgredgedgloop  28228  cusgrfilem2  28453  nsgqusf1olem2  32247  ghmquskerlem2  32252  ssmxidl  32294  cmppcmp  32503  eulerpartlemgvv  33040  eulerpartlemgh  33042  fnrelpredd  33757  erdszelem7  33855  rellysconn  33909  ivthALT  34860  fnessref  34882  phpreu  36112  poimirlem26  36154  itg2gt0cn  36183  frinfm  36244  sstotbnd2  36283  heiborlem3  36322  isdrngo3  36468  dihjat1lem  39941  dvh1dim  39955  dochsatshp  39964  mapdpglem2  40186  prjspreln0  40994  pellexlem5  41203  pell14qrss1234  41226  pell1qrss14  41238  lnr2i  41490  hbtlem6  41503  dflim5  41711  naddgeoa  41758  mnuop3d  42643  fvelsetpreimafv  45669  opnneir  47029
  Copyright terms: Public domain W3C validator