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

Theorem reximdv2 3194
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 1960 . 2 (𝜑 → (∃𝑥(𝑥𝐴𝜓) → ∃𝑥(𝑥𝐵𝜒)))
3 df-rex 3095 . 2 (∃𝑥𝐴 𝜓 ↔ ∃𝑥(𝑥𝐴𝜓))
4 df-rex 3095 . 2 (∃𝑥𝐵 𝜒 ↔ ∃𝑥(𝑥𝐵𝜒))
52, 3, 43imtr4g 288 1 (𝜑 → (∃𝑥𝐴 𝜓 → ∃𝑥𝐵 𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  wex 1823  wcel 2106  wrex 3090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953
This theorem depends on definitions:  df-bi 199  df-ex 1824  df-rex 3095
This theorem is referenced by:  reximssdv  3199  ssrexv  3885  ssimaex  6523  nnsuc  7360  oaass  7925  omeulem1  7946  ssnnfi  8467  findcard3  8491  unfilem1  8512  epfrs  8904  alephval3  9266  isfin7-2  9553  fpwwe2lem13  9799  inawinalem  9846  ico0  12533  ioc0  12534  r19.2uz  14498  climrlim2  14686  iserodd  15944  ramub2  16122  prmgaplem6  16164  ablfaclem3  18873  unitgrp  19054  restnlly  21694  llyrest  21697  nllyrest  21698  llyidm  21700  nllyidm  21701  cnpflfi  22211  cnextcn  22279  ivthlem3  23657  dvfsumrlim  24231  lgsquadlem2  25558  footex  26069  oppperpex  26101  outpasch  26103  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  cusgrfilem2  26804  cmppcmp  30523  eulerpartlemgvv  31036  eulerpartlemgh  31038  erdszelem7  31778  rellysconn  31832  trpredrec  32326  ivthALT  32918  fnessref  32940  phpreu  34002  poimirlem26  34045  itg2gt0cn  34074  frinfm  34139  sstotbnd2  34181  heiborlem3  34220  isdrngo3  34366  dihjat1lem  37566  dvh1dim  37580  dochsatshp  37589  mapdpglem2  37811  pellexlem5  38339  pell14qrss1234  38362  pell1qrss14  38374  lnr2i  38627  hbtlem6  38640
  Copyright terms: Public domain W3C validator