![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximdv2 | Structured version Visualization version GIF version |
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 17-Sep-2003.) |
Ref | Expression |
---|---|
reximdv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) |
Ref | Expression |
---|---|
reximdv2 | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximdv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) → (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
2 | 1 | eximdv 1886 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 2947 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 2947 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 285 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∃wex 1744 ∈ wcel 2030 ∃wrex 2942 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 |
This theorem depends on definitions: df-bi 197 df-ex 1745 df-rex 2947 |
This theorem is referenced by: ssrexv 3700 ssimaex 6302 nnsuc 7124 oaass 7686 omeulem1 7707 ssnnfi 8220 findcard3 8244 unfilem1 8265 epfrs 8645 alephval3 8971 isfin7-2 9256 fin1a2lem6 9265 fpwwe2lem12 9501 fpwwe2lem13 9502 inawinalem 9549 ico0 12259 ioc0 12260 r19.2uz 14135 climrlim2 14322 iserodd 15587 ramub2 15765 prmgaplem6 15807 pgpssslw 18075 efgrelexlemb 18209 ablfaclem3 18532 unitgrp 18713 lspsneq 19170 lbsextlem4 19209 neissex 20979 iscnp4 21115 nlly2i 21327 llynlly 21328 restnlly 21333 llyrest 21336 nllyrest 21337 llyidm 21339 nllyidm 21340 qtophmeo 21668 cnpflfi 21850 cnextcn 21918 ivthlem3 23268 ovolicc2lem5 23335 dvfsumrlim 23839 itgsubst 23857 lgsquadlem2 25151 footex 25658 opphllem1 25684 oppperpex 25690 outpasch 25692 ushgredgedg 26166 ushgredgedgloop 26168 cusgrfilem2 26408 cmppcmp 30053 eulerpartlemgvv 30566 eulerpartlemgh 30568 erdszelem7 31305 rellysconn 31359 trpredrec 31862 ivthALT 32455 fnessref 32477 phpreu 33523 poimirlem26 33565 itg2gt0cn 33595 frinfm 33660 sstotbnd2 33703 heiborlem3 33742 isdrngo3 33888 dihjat1lem 37034 dvh1dim 37048 dochsatshp 37057 lcfl6 37106 mapdval2N 37236 mapdpglem2 37279 hdmaprnlem10N 37468 pellexlem5 37714 pell14qrss1234 37737 pell1qrss14 37749 pellfundglb 37766 lnr2i 38003 hbtlem6 38016 |
Copyright terms: Public domain | W3C validator |