Theorem reximi2 3096

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

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

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

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

This theorem is used by:  reximia  3098  pssnn  9168  btwnz  12783  xrsupexmnf  13416  xrinfmexpnf  13417  xrsupsslem  13418  xrinfmsslem  13419  supxrun  13427  ioo0  13482  hashgt23el  14549  resqrex  15397  resqreu  15399  rexuzre  15500  neiptopnei  23430  comppfsc  23831  filssufilg  24210  alexsubALTlem4  24349  lgsquadlem2  27690  nmobndseqi  31363  nmobndseqiALT  31364  pjnmopi  32732  crefdf  34462  dya2iocuni  34898  ballotlemfc0  35108  ballotlemfcc  35109  ballotlemsup  35120  fnrelpredd  35699  poimirlem32  38538  sstotbnd3  38678  lsateln0  40020  pclcmpatN  40926  aaitgo  44122  stoweidlem14  46968  stoweidlem57  47011  elaa2  47188