Theorem reximi2 2993

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

Syntax hints:   → wi 4   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-rex 2902

This theorem is referenced by:  pssnn  8063  btwnz  11355  xrsupexmnf  12007  xrinfmexpnf  12008  xrsupsslem  12009  xrinfmsslem  12010  supxrun  12018  ioo0  12071  resqrex  13839  resqreu  13841  rexuzre  13940  neiptopnei  20746  comppfsc  21145  filssufilg  21525  alexsubALTlem4  21664  lgsquadlem2  24906  nmobndseqi  27018  nmobndseqiALT  27019  pjnmopi  28391  crefdf  29243  dya2iocuni  29672  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsup  29893  poimirlem32  32611  sstotbnd3  32745  lsateln0  33300  pclcmpatN  34205  aaitgo  36751  stoweidlem14  38907  stoweidlem57  38950  elaa2  39127