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  9132  btwnz  12637  xrsupexmnf  13265  xrinfmexpnf  13266  xrsupsslem  13267  xrinfmsslem  13268  supxrun  13276  ioo0  13331  hashgt23el  14389  resqrex  15216  resqreu  15218  rexuzre  15319  neiptopnei  23019  comppfsc  23419  filssufilg  23798  alexsubALTlem4  23937  lgsquadlem2  27292  nmobndseqi  30708  nmobndseqiALT  30709  pjnmopi  32077  crefdf  33838  dya2iocuni  34274  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsup  34496  fnrelpredd  35079  poimirlem32  37646  sstotbnd3  37770  lsateln0  38988  pclcmpatN  39895  aaitgo  43151  stoweidlem14  46012  stoweidlem57  46055  elaa2  46232