Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reximi2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 8-Nov-2004.) |
Ref | Expression |
---|---|
reximi2.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) |
Ref | Expression |
---|---|
reximi2 | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximi2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → (𝑥 ∈ 𝐵 ∧ 𝜓)) | |
2 | 1 | eximi 1826 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3141 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3141 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 293 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∃wex 1771 ∈ wcel 2105 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ex 1772 df-rex 3141 |
This theorem is referenced by: pssnn 8724 btwnz 12072 xrsupexmnf 12686 xrinfmexpnf 12687 xrsupsslem 12688 xrinfmsslem 12689 supxrun 12697 ioo0 12751 hashgt23el 13773 resqrex 14598 resqreu 14600 rexuzre 14700 neiptopnei 21668 comppfsc 22068 filssufilg 22447 alexsubALTlem4 22586 lgsquadlem2 25884 nmobndseqi 28483 nmobndseqiALT 28484 pjnmopi 29852 crefdf 31011 dya2iocuni 31440 ballotlemfc0 31649 ballotlemfcc 31650 ballotlemsup 31661 poimirlem32 34805 sstotbnd3 34935 lsateln0 36011 pclcmpatN 36917 aaitgo 39640 stoweidlem14 42176 stoweidlem57 42219 elaa2 42396 |
Copyright terms: Public domain | W3C validator |