Theorem reximi2 3062

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3054

This theorem is referenced by:  reximia  3064  pssnn  9092  btwnz  12597  xrsupexmnf  13225  xrinfmexpnf  13226  xrsupsslem  13227  xrinfmsslem  13228  supxrun  13236  ioo0  13291  hashgt23el  14349  resqrex  15175  resqreu  15177  rexuzre  15278  neiptopnei  23035  comppfsc  23435  filssufilg  23814  alexsubALTlem4  23953  lgsquadlem2  27308  nmobndseqi  30741  nmobndseqiALT  30742  pjnmopi  32110  crefdf  33814  dya2iocuni  34250  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemsup  34472  fnrelpredd  35055  poimirlem32  37631  sstotbnd3  37755  lsateln0  38973  pclcmpatN  39880  aaitgo  43135  stoweidlem14  45996  stoweidlem57  46039  elaa2  46216