Theorem reximi2 3174

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2110  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 206  df-ex 1787  df-rex 3072

This theorem is referenced by:  reximia  3175  pssnn  8933  pssnnOLD  9018  btwnz  12422  xrsupexmnf  13038  xrinfmexpnf  13039  xrsupsslem  13040  xrinfmsslem  13041  supxrun  13049  ioo0  13103  hashgt23el  14137  resqrex  14960  resqreu  14962  rexuzre  15062  neiptopnei  22281  comppfsc  22681  filssufilg  23060  alexsubALTlem4  23199  lgsquadlem2  26527  nmobndseqi  29137  nmobndseqiALT  29138  pjnmopi  30506  crefdf  31794  dya2iocuni  32246  ballotlemfc0  32455  ballotlemfcc  32456  ballotlemsup  32467  fnrelpredd  33057  poimirlem32  35805  sstotbnd3  35930  lsateln0  37005  pclcmpatN  37911  aaitgo  40984  stoweidlem14  43526  stoweidlem57  43569  elaa2  43746