Theorem reximi2 3080

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

Syntax hints:   → wi 4   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

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

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

This theorem is referenced by:  reximia  3082  pssnn  9168  pssnnOLD  9265  btwnz  12665  xrsupexmnf  13284  xrinfmexpnf  13285  xrsupsslem  13286  xrinfmsslem  13287  supxrun  13295  ioo0  13349  hashgt23el  14384  resqrex  15197  resqreu  15199  rexuzre  15299  neiptopnei  22636  comppfsc  23036  filssufilg  23415  alexsubALTlem4  23554  lgsquadlem2  26884  nmobndseqi  30032  nmobndseqiALT  30033  pjnmopi  31401  crefdf  32828  dya2iocuni  33282  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemsup  33503  fnrelpredd  34092  poimirlem32  36520  sstotbnd3  36644  lsateln0  37865  pclcmpatN  38772  aaitgo  41904  stoweidlem14  44730  stoweidlem57  44773  elaa2  44950