Theorem reximi2 3167

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 1842	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
3		df-rex 3067	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 3067	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
5	2, 3, 4	3imtr4i 295	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1787   ∈ wcel 2110  ∃wrex 3062

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

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-rex 3067

This theorem is referenced by:  pssnn  8846  pssnnOLD  8895  btwnz  12279  xrsupexmnf  12895  xrinfmexpnf  12896  xrsupsslem  12897  xrinfmsslem  12898  supxrun  12906  ioo0  12960  hashgt23el  13991  resqrex  14814  resqreu  14816  rexuzre  14916  neiptopnei  22029  comppfsc  22429  filssufilg  22808  alexsubALTlem4  22947  lgsquadlem2  26262  nmobndseqi  28860  nmobndseqiALT  28861  pjnmopi  30229  crefdf  31512  dya2iocuni  31962  ballotlemfc0  32171  ballotlemfcc  32172  ballotlemsup  32183  fnrelpredd  32774  poimirlem32  35546  sstotbnd3  35671  lsateln0  36746  pclcmpatN  37652  aaitgo  40690  stoweidlem14  43230  stoweidlem57  43273  elaa2  43450