Theorem reximdv2 3150

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

Step	Hyp	Ref	Expression
1		reximdv2.1	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒)))
2	1	eximdv 1924	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 297	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-rex 3065

This theorem is referenced by:  reximdvai  3151  reximssdv  3158  ssimaex  6919  nnsuc  7831  oaass  8493  omeulem1  8514  ssnnfi  9101  findcard3  9190  unfilem1  9212  epfrs  9650  alephval3  10030  isfin7-2  10316  fpwwe2lem12  10563  inawinalem  10610  ico0  13342  ioc0  13343  r19.2uz  15312  climrlim2  15507  prmdvdsncoprmbd  16695  iserodd  16804  ramub2  16983  prmgaplem6  17025  ghmqusnsglem2  19254  ghmquskerlem2  19258  ablfaclem3  20062  unitgrp  20361  restnlly  23472  llyrest  23475  nllyrest  23476  llyidm  23478  nllyidm  23479  cnpflfi  23989  cnextcn  24057  ivthlem3  25445  dvfsumrlim  26023  lgsquadlem2  27369  oppperpex  28846  outpasch  28848  ushgredgedg  29323  ushgredgedgloop  29325  cusgrfilem2  29550  nsgqusf1olem2  33504  ssmxidl  33564  cmppcmp  34049  eulerpartlemgvv  34567  eulerpartlemgh  34569  fnrelpredd  35279  r1filimi  35291  noinfepfnregs  35320  erdszelem7  35432  rellysconn  35486  ivthALT  36570  fnessref  36592  phpreu  37978  poimirlem26  38020  itg2gt0cn  38049  frinfm  38109  sstotbnd2  38148  heiborlem3  38187  isdrngo3  38333  dihjat1lem  41927  dvh1dim  41941  dochsatshp  41950  mapdpglem2  42172  prjspreln0  43066  pellexlem5  43285  pell14qrss1234  43308  pell1qrss14  43320  lnr2i  43568  hbtlem6  43581  dflim5  43781  tfsconcatrn  43794  naddgeoa  43846  mnuop3d  44722  fvelsetpreimafv  47869  opnneir  49404