![]() |
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 1830 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3061 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3061 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 291 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∃wex 1774 ∈ wcel 2099 ∃wrex 3060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-ex 1775 df-rex 3061 |
This theorem is referenced by: reximia 3071 pssnn 9206 pssnnOLD 9299 btwnz 12717 xrsupexmnf 13338 xrinfmexpnf 13339 xrsupsslem 13340 xrinfmsslem 13341 supxrun 13349 ioo0 13403 hashgt23el 14441 resqrex 15255 resqreu 15257 rexuzre 15357 neiptopnei 23127 comppfsc 23527 filssufilg 23906 alexsubALTlem4 24045 lgsquadlem2 27410 nmobndseqi 30712 nmobndseqiALT 30713 pjnmopi 32081 crefdf 33663 dya2iocuni 34117 ballotlemfc0 34326 ballotlemfcc 34327 ballotlemsup 34338 fnrelpredd 34926 poimirlem32 37353 sstotbnd3 37477 lsateln0 38693 pclcmpatN 39600 aaitgo 42823 stoweidlem14 45635 stoweidlem57 45678 elaa2 45855 |
Copyright terms: Public domain | W3C validator |