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 1912 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) → ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3065 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3065 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 296 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wex 1773  wcel 2098  wrex 3064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905
This theorem depends on definitions:  df-bi 206  df-ex 1774  df-rex 3065
This theorem is referenced by:  reximdvai  3159  reximssdv  3166  ssrexv  4046  ssimaex  6970  nnsuc  7870  oaass  8562  omeulem1  8583  ssnnfi  9171  ssnnfiOLD  9172  findcard3  9287  findcard3OLD  9288  unfilem1  9312  epfrs  9728  alephval3  10107  isfin7-2  10393  fpwwe2lem12  10639  inawinalem  10686  ico0  13376  ioc0  13377  r19.2uz  15304  climrlim2  15497  prmdvdsncoprmbd  16672  iserodd  16777  ramub2  16956  prmgaplem6  16998  ablfaclem3  20009  unitgrp  20285  restnlly  23341  llyrest  23344  nllyrest  23345  llyidm  23347  nllyidm  23348  cnpflfi  23858  cnextcn  23926  ivthlem3  25337  dvfsumrlim  25921  lgsquadlem2  27269  oppperpex  28512  outpasch  28514  ushgredgedg  28994  ushgredgedgloop  28996  cusgrfilem2  29222  nsgqusf1olem2  33031  ghmquskerlem2  33036  ssmxidl  33096  cmppcmp  33368  eulerpartlemgvv  33905  eulerpartlemgh  33907  fnrelpredd  34621  erdszelem7  34716  rellysconn  34770  ivthALT  35728  fnessref  35750  phpreu  36985  poimirlem26  37027  itg2gt0cn  37056  frinfm  37116  sstotbnd2  37155  heiborlem3  37194  isdrngo3  37340  dihjat1lem  40812  dvh1dim  40826  dochsatshp  40835  mapdpglem2  41057  prjspreln0  41929  pellexlem5  42149  pell14qrss1234  42172  pell1qrss14  42184  lnr2i  42436  hbtlem6  42449  dflim5  42655  tfsconcatrn  42668  naddgeoa  42721  mnuop3d  43606  fvelsetpreimafv  46627  opnneir  47813
  Copyright terms: Public domain W3C validator