Theorem reximi2 3197

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

Syntax hints:   → wi 4   ∧ wa 384  ∃wex 1859   ∈ wcel 2156  ∃wrex 3097

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

This theorem depends on definitions:  df-bi 198  df-ex 1860  df-rex 3102

This theorem is referenced by:  pssnn  8413  btwnz  11741  xrsupexmnf  12349  xrinfmexpnf  12350  xrsupsslem  12351  xrinfmsslem  12352  supxrun  12360  ioo0  12414  resqrex  14210  resqreu  14212  rexuzre  14311  neiptopnei  21147  comppfsc  21546  filssufilg  21925  alexsubALTlem4  22064  lgsquadlem2  25319  nmobndseqi  27961  nmobndseqiALT  27962  pjnmopi  29334  crefdf  30239  dya2iocuni  30669  ballotlemfc0  30878  ballotlemfcc  30879  ballotlemsup  30890  poimirlem32  33752  sstotbnd3  33884  lsateln0  34773  pclcmpatN  35679  aaitgo  38230  stoweidlem14  40707  stoweidlem57  40750  elaa2  40927