Theorem reximi2 3101

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

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

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 3093

This theorem is used by:  reximia  3103  pssnn  9163  btwnz  12717  xrsupexmnf  13349  xrinfmexpnf  13350  xrsupsslem  13351  xrinfmsslem  13352  supxrun  13360  ioo0  13415  hashgt23el  14481  resqrex  15327  resqreu  15329  rexuzre  15430  neiptopnei  23326  comppfsc  23726  filssufilg  24105  alexsubALTlem4  24244  lgsquadlem2  27582  nmobndseqi  31168  nmobndseqiALT  31169  pjnmopi  32537  crefdf  34269  dya2iocuni  34705  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemsup  34927  fnrelpredd  35507  poimirlem32  38344  sstotbnd3  38468  lsateln0  39810  pclcmpatN  40716  aaitgo  43930  stoweidlem14  46769  stoweidlem57  46812  elaa2  46989