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 1858	. 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 1802   ∈ wcel 2145  ∃wrex 3089

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

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

This theorem is referenced by:  reximia  3100  pssnn  9141  btwnz  12690  xrsupexmnf  13322  xrinfmexpnf  13323  xrsupsslem  13324  xrinfmsslem  13325  supxrun  13333  ioo0  13388  hashgt23el  14451  resqrex  15291  resqreu  15293  rexuzre  15394  neiptopnei  23250  comppfsc  23650  filssufilg  24029  alexsubALTlem4  24168  lgsquadlem2  27503  nmobndseqi  31040  nmobndseqiALT  31041  pjnmopi  32409  crefdf  34155  dya2iocuni  34590  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemsup  34812  fnrelpredd  35397  poimirlem32  38163  sstotbnd3  38287  lsateln0  39631  pclcmpatN  40537  aaitgo  43751  stoweidlem14  46586  stoweidlem57  46629  elaa2  46806