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 1838 | . 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) |
3 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) | |
4 | df-rex 3069 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 291 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1783 ∈ wcel 2108 ∃wrex 3064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 |
This theorem depends on definitions: df-bi 206 df-ex 1784 df-rex 3069 |
This theorem is referenced by: reximia 3172 pssnn 8913 pssnnOLD 8969 btwnz 12352 xrsupexmnf 12968 xrinfmexpnf 12969 xrsupsslem 12970 xrinfmsslem 12971 supxrun 12979 ioo0 13033 hashgt23el 14067 resqrex 14890 resqreu 14892 rexuzre 14992 neiptopnei 22191 comppfsc 22591 filssufilg 22970 alexsubALTlem4 23109 lgsquadlem2 26434 nmobndseqi 29042 nmobndseqiALT 29043 pjnmopi 30411 crefdf 31700 dya2iocuni 32150 ballotlemfc0 32359 ballotlemfcc 32360 ballotlemsup 32371 fnrelpredd 32961 poimirlem32 35736 sstotbnd3 35861 lsateln0 36936 pclcmpatN 37842 aaitgo 40903 stoweidlem14 43445 stoweidlem57 43488 elaa2 43665 |
Copyright terms: Public domain | W3C validator |