Theorem reximi2 3099

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

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

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 3091

This theorem is used by:  reximia  3101  pssnn  9212  btwnz  12829  xrsupexmnf  13462  xrinfmexpnf  13463  xrsupsslem  13464  xrinfmsslem  13465  supxrun  13473  ioo0  13528  hashgt23el  14596  resqrex  15446  resqreu  15448  rexuzre  15549  neiptopnei  23480  comppfsc  23881  filssufilg  24260  alexsubALTlem4  24399  lgsquadlem2  27738  nmobndseqi  31411  nmobndseqiALT  31412  pjnmopi  32780  crefdf  34550  dya2iocuni  34985  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemsup  35207  fnrelpredd  35804  poimirlem32  38762  sstotbnd3  38902  lsateln0  40244  pclcmpatN  41150  aaitgo  44356  stoweidlem14  47229  stoweidlem57  47272  elaa2  47449