![]() |
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 1921 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3071 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 296 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∃wex 1782 ∈ wcel 2107 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-ex 1783 df-rex 3071 |
This theorem is referenced by: reximdvai 3159 reximssdv 3166 ssrexv 4015 ssimaex 6930 nnsuc 7824 oaass 8512 omeulem1 8533 ssnnfi 9119 ssnnfiOLD 9120 findcard3 9235 findcard3OLD 9236 unfilem1 9260 epfrs 9675 alephval3 10054 isfin7-2 10340 fpwwe2lem12 10586 inawinalem 10633 ico0 13319 ioc0 13320 r19.2uz 15245 climrlim2 15438 prmdvdsncoprmbd 16610 iserodd 16715 ramub2 16894 prmgaplem6 16936 ablfaclem3 19874 unitgrp 20104 restnlly 22856 llyrest 22859 nllyrest 22860 llyidm 22862 nllyidm 22863 cnpflfi 23373 cnextcn 23441 ivthlem3 24840 dvfsumrlim 25418 lgsquadlem2 26752 oppperpex 27744 outpasch 27746 ushgredgedg 28226 ushgredgedgloop 28228 cusgrfilem2 28453 nsgqusf1olem2 32247 ghmquskerlem2 32252 ssmxidl 32294 cmppcmp 32503 eulerpartlemgvv 33040 eulerpartlemgh 33042 fnrelpredd 33757 erdszelem7 33855 rellysconn 33909 ivthALT 34860 fnessref 34882 phpreu 36112 poimirlem26 36154 itg2gt0cn 36183 frinfm 36244 sstotbnd2 36283 heiborlem3 36322 isdrngo3 36468 dihjat1lem 39941 dvh1dim 39955 dochsatshp 39964 mapdpglem2 40186 prjspreln0 40994 pellexlem5 41203 pell14qrss1234 41226 pell1qrss14 41238 lnr2i 41490 hbtlem6 41503 dflim5 41711 naddgeoa 41758 mnuop3d 42643 fvelsetpreimafv 45669 opnneir 47029 |
Copyright terms: Public domain | W3C validator |