Theorem reximi2 3073

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-rex 3065

This theorem is referenced by:  reximia  3075  pssnn  9100  btwnz  12630  xrsupexmnf  13255  xrinfmexpnf  13256  xrsupsslem  13257  xrinfmsslem  13258  supxrun  13266  ioo0  13321  hashgt23el  14384  resqrex  15210  resqreu  15212  rexuzre  15313  neiptopnei  23122  comppfsc  23522  filssufilg  23901  alexsubALTlem4  24040  lgsquadlem2  27369  nmobndseqi  30875  nmobndseqiALT  30876  pjnmopi  32244  crefdf  34039  dya2iocuni  34474  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemsup  34696  fnrelpredd  35279  poimirlem32  38026  sstotbnd3  38150  lsateln0  39494  pclcmpatN  40400  aaitgo  43614  stoweidlem14  46464  stoweidlem57  46507  elaa2  46684