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

Theorem reximdv2 3275
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 1911 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) → ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3148 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3148 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 297 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1773  wcel 2107  wrex 3143
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 1904
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-rex 3148
This theorem is referenced by:  reximssdv  3280  ssrexv  4037  ssimaex  6744  nnsuc  7588  oaass  8180  omeulem1  8201  ssnnfi  8729  findcard3  8753  unfilem1  8774  epfrs  9165  alephval3  9528  isfin7-2  9810  fpwwe2lem13  10056  inawinalem  10103  ico0  12777  ioc0  12778  r19.2uz  14704  climrlim2  14897  iserodd  16164  ramub2  16342  prmgaplem6  16384  ablfaclem3  19131  unitgrp  19339  restnlly  22008  llyrest  22011  nllyrest  22012  llyidm  22014  nllyidm  22015  cnpflfi  22525  cnextcn  22593  ivthlem3  23971  dvfsumrlim  24545  lgsquadlem2  25873  oppperpex  26455  outpasch  26457  ushgredgedg  26927  ushgredgedgloop  26929  cusgrfilem2  27154  cmppcmp  31010  eulerpartlemgvv  31522  eulerpartlemgh  31524  erdszelem7  32330  rellysconn  32384  trpredrec  32963  ivthALT  33569  fnessref  33591  phpreu  34745  poimirlem26  34787  itg2gt0cn  34816  frinfm  34880  sstotbnd2  34922  heiborlem3  34961  isdrngo3  35107  dihjat1lem  38433  dvh1dim  38447  dochsatshp  38456  mapdpglem2  38678  prjspreln0  39126  pellexlem5  39297  pell14qrss1234  39320  pell1qrss14  39332  lnr2i  39583  hbtlem6  39596  mnuop3d  40474
  Copyright terms: Public domain W3C validator