Theorem reximi2 3079

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

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

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-rex 3071

This theorem is referenced by:  reximia  3081  pssnn  9170  pssnnOLD  9267  btwnz  12669  xrsupexmnf  13288  xrinfmexpnf  13289  xrsupsslem  13290  xrinfmsslem  13291  supxrun  13299  ioo0  13353  hashgt23el  14388  resqrex  15201  resqreu  15203  rexuzre  15303  neiptopnei  22856  comppfsc  23256  filssufilg  23635  alexsubALTlem4  23774  lgsquadlem2  27108  nmobndseqi  30287  nmobndseqiALT  30288  pjnmopi  31656  crefdf  33114  dya2iocuni  33568  ballotlemfc0  33777  ballotlemfcc  33778  ballotlemsup  33789  fnrelpredd  34378  poimirlem32  36823  sstotbnd3  36947  lsateln0  38168  pclcmpatN  39075  aaitgo  42206  stoweidlem14  45029  stoweidlem57  45072  elaa2  45249