Theorem reximdv2 3230

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 1918	. 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)))
3		df-rex 3112	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓))
4		df-rex 3112	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))
5	2, 3, 4	3imtr4g 299	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒))

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-rex 3112

This theorem is referenced by:  reximssdv  3235  ssrexv  3982  ssimaex  6723  nnsuc  7577  oaass  8170  omeulem1  8191  ssnnfi  8721  findcard3  8745  unfilem1  8766  epfrs  9157  alephval3  9521  isfin7-2  9807  fpwwe2lem13  10053  inawinalem  10100  ico0  12772  ioc0  12773  r19.2uz  14703  climrlim2  14896  iserodd  16162  ramub2  16340  prmgaplem6  16382  ablfaclem3  19202  unitgrp  19413  restnlly  22087  llyrest  22090  nllyrest  22091  llyidm  22093  nllyidm  22094  cnpflfi  22604  cnextcn  22672  ivthlem3  24057  dvfsumrlim  24634  lgsquadlem2  25965  oppperpex  26547  outpasch  26549  ushgredgedg  27019  ushgredgedgloop  27021  cusgrfilem2  27246  ssmxidl  31050  cmppcmp  31211  eulerpartlemgvv  31744  eulerpartlemgh  31746  fnrelpredd  32472  erdszelem7  32557  rellysconn  32611  trpredrec  33190  ivthALT  33796  fnessref  33818  phpreu  35041  poimirlem26  35083  itg2gt0cn  35112  frinfm  35173  sstotbnd2  35212  heiborlem3  35251  isdrngo3  35397  dihjat1lem  38724  dvh1dim  38738  dochsatshp  38747  mapdpglem2  38969  prjspreln0  39603  pellexlem5  39774  pell14qrss1234  39797  pell1qrss14  39809  lnr2i  40060  hbtlem6  40073  mnuop3d  40979  fvelsetpreimafv  43904