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 1841 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3072 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3072 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 292 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |