Theorem reximdv2 3271

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139

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

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-rex 3144

This theorem is referenced by:  reximssdv  3276  ssrexv  4034  ssimaex  6748  nnsuc  7597  oaass  8187  omeulem1  8208  ssnnfi  8737  findcard3  8761  unfilem1  8782  epfrs  9173  alephval3  9536  isfin7-2  9818  fpwwe2lem13  10064  inawinalem  10111  ico0  12785  ioc0  12786  r19.2uz  14711  climrlim2  14904  iserodd  16172  ramub2  16350  prmgaplem6  16392  ablfaclem3  19209  unitgrp  19417  restnlly  22090  llyrest  22093  nllyrest  22094  llyidm  22096  nllyidm  22097  cnpflfi  22607  cnextcn  22675  ivthlem3  24054  dvfsumrlim  24628  lgsquadlem2  25957  oppperpex  26539  outpasch  26541  ushgredgedg  27011  ushgredgedgloop  27013  cusgrfilem2  27238  ssmxidl  30979  cmppcmp  31122  eulerpartlemgvv  31634  eulerpartlemgh  31636  erdszelem7  32444  rellysconn  32498  trpredrec  33077  ivthALT  33683  fnessref  33705  phpreu  34891  poimirlem26  34933  itg2gt0cn  34962  frinfm  35025  sstotbnd2  35067  heiborlem3  35106  isdrngo3  35252  dihjat1lem  38579  dvh1dim  38593  dochsatshp  38602  mapdpglem2  38824  prjspreln0  39279  pellexlem5  39450  pell14qrss1234  39473  pell1qrss14  39485  lnr2i  39736  hbtlem6  39749  mnuop3d  40627  fvelsetpreimafv  43567