Theorem reximi2 3069

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

Syntax hints:   → wi 4   ∧ wa 394  ∃wex 1774   ∈ wcel 2099  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-rex 3061

This theorem is referenced by:  reximia  3071  pssnn  9206  pssnnOLD  9299  btwnz  12717  xrsupexmnf  13338  xrinfmexpnf  13339  xrsupsslem  13340  xrinfmsslem  13341  supxrun  13349  ioo0  13403  hashgt23el  14441  resqrex  15255  resqreu  15257  rexuzre  15357  neiptopnei  23127  comppfsc  23527  filssufilg  23906  alexsubALTlem4  24045  lgsquadlem2  27410  nmobndseqi  30712  nmobndseqiALT  30713  pjnmopi  32081  crefdf  33663  dya2iocuni  34117  ballotlemfc0  34326  ballotlemfcc  34327  ballotlemsup  34338  fnrelpredd  34926  poimirlem32  37353  sstotbnd3  37477  lsateln0  38693  pclcmpatN  39600  aaitgo  42823  stoweidlem14  45635  stoweidlem57  45678  elaa2  45855