Theorem reximi2 3098

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-rex 3090

This theorem is referenced by:  reximia  3100  pssnn  9154  btwnz  12700  xrsupexmnf  13332  xrinfmexpnf  13333  xrsupsslem  13334  xrinfmsslem  13335  supxrun  13343  ioo0  13398  hashgt23el  14463  resqrex  15303  resqreu  15305  rexuzre  15406  neiptopnei  23270  comppfsc  23670  filssufilg  24049  alexsubALTlem4  24188  lgsquadlem2  27523  nmobndseqi  31109  nmobndseqiALT  31110  pjnmopi  32478  crefdf  34216  dya2iocuni  34651  ballotlemfc0  34861  ballotlemfcc  34862  ballotlemsup  34873  fnrelpredd  35460  poimirlem32  38281  sstotbnd3  38405  lsateln0  39747  pclcmpatN  40653  aaitgo  43869  stoweidlem14  46708  stoweidlem57  46751  elaa2  46928