Theorem reximdv2 3178

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3093

This theorem is used by:  reximdvai  3179  reximssdv  3186  ssimaex  6973  nnsuc  7889  oaass  8555  omeulem1  8576  ssnnfi  9164  findcard3  9253  unfilem1  9275  epfrs  9710  alephval3  10113  isfin7-2  10398  fpwwe2lem12  10645  inawinalem  10692  ico0  13436  ioc0  13437  r19.2uz  15429  climrlim2  15624  prmdvdsncoprmbd  16811  iserodd  16920  ramub2  17099  prmgaplem6  17141  ghmqusnsglem2  19382  ghmquskerlem2  19386  ablfaclem3  20190  unitgrp  20498  isdrng5  20891  restnlly  23676  llyrest  23679  nllyrest  23680  llyidm  23682  nllyidm  23683  cnpflfi  24193  cnextcn  24261  ivthlem3  25649  dvfsumrlim  26227  lgsquadlem2  27582  tglnpt3  28964  tglnpt4  28965  oppperpex  29071  outpasch  29074  ushgredgedg  29616  ushgredgedgloop  29618  cusgrfilem2  29843  nsgqusf1olem2  33754  ssmxidl  33788  cmppcmp  34279  eulerpartlemgvv  34798  eulerpartlemgh  34800  fnrelpredd  35507  r1filimi  35522  noinfepfnregs  35569  erdszelem7  35710  rellysconn  35764  ivthALT  36887  fnessref  36909  phpreu  38296  poimirlem26  38338  itg2gt0cn  38367  frinfm  38427  sstotbnd2  38466  heiborlem3  38505  isdrngo3  38651  dihjat1lem  42243  dvh1dim  42257  dochsatshp  42266  mapdpglem2  42488  prjspreln0  43382  pellexlem5  43601  pell14qrss1234  43624  pell1qrss14  43636  lnr2i  43884  hbtlem6  43897  dflim5  44097  tfsconcatrn  44110  naddgeoa  44162  mnuop3d  45022  fvelsetpreimafv  48177  opnneir  49726