Theorem reximi2 3185

Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.)

Hypothesis

Ref	Expression
reximi2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))

Assertion

Ref	Expression
reximi2	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Proof of Theorem reximi2

Step	Hyp	Ref	Expression
1		reximi2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓))
2	1	eximi 1797	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
3		df-rex 3088	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 3088	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
5	2, 3, 4	3imtr4i 284	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 387  ∃wex 1742   ∈ wcel 2048  ∃wrex 3083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772

This theorem depends on definitions:  df-bi 199  df-ex 1743  df-rex 3088

This theorem is referenced by:  pssnn  8523  btwnz  11890  xrsupexmnf  12507  xrinfmexpnf  12508  xrsupsslem  12509  xrinfmsslem  12510  supxrun  12518  ioo0  12572  resqrex  14461  resqreu  14463  rexuzre  14563  neiptopnei  21434  comppfsc  21834  filssufilg  22213  alexsubALTlem4  22352  lgsquadlem2  25649  nmobndseqi  28323  nmobndseqiALT  28324  pjnmopi  29696  crefdf  30713  dya2iocuni  31143  ballotlemfc0  31353  ballotlemfcc  31354  ballotlemsup  31365  poimirlem32  34313  sstotbnd3  34444  lsateln0  35524  pclcmpatN  36430  aaitgo  39103  stoweidlem14  41676  stoweidlem57  41719  elaa2  41896