![]() |
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 1919 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3070 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 296 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∃wex 1780 ∈ wcel 2105 ∃wrex 3069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 |
This theorem depends on definitions: df-bi 206 df-ex 1781 df-rex 3070 |
This theorem is referenced by: reximdvai 3164 reximssdv 3171 ssrexv 4051 ssimaex 6976 nnsuc 7877 oaass 8567 omeulem1 8588 ssnnfi 9175 ssnnfiOLD 9176 findcard3 9291 findcard3OLD 9292 unfilem1 9316 epfrs 9732 alephval3 10111 isfin7-2 10397 fpwwe2lem12 10643 inawinalem 10690 ico0 13377 ioc0 13378 r19.2uz 15305 climrlim2 15498 prmdvdsncoprmbd 16670 iserodd 16775 ramub2 16954 prmgaplem6 16996 ablfaclem3 20005 unitgrp 20281 restnlly 23306 llyrest 23309 nllyrest 23310 llyidm 23312 nllyidm 23313 cnpflfi 23823 cnextcn 23891 ivthlem3 25302 dvfsumrlim 25886 lgsquadlem2 27227 oppperpex 28437 outpasch 28439 ushgredgedg 28919 ushgredgedgloop 28921 cusgrfilem2 29146 nsgqusf1olem2 32965 ghmquskerlem2 32970 ssmxidl 33030 cmppcmp 33302 eulerpartlemgvv 33839 eulerpartlemgh 33841 fnrelpredd 34556 erdszelem7 34652 rellysconn 34706 ivthALT 35684 fnessref 35706 phpreu 36936 poimirlem26 36978 itg2gt0cn 37007 frinfm 37067 sstotbnd2 37106 heiborlem3 37145 isdrngo3 37291 dihjat1lem 40763 dvh1dim 40777 dochsatshp 40786 mapdpglem2 41008 prjspreln0 41814 pellexlem5 42034 pell14qrss1234 42057 pell1qrss14 42069 lnr2i 42321 hbtlem6 42334 dflim5 42542 tfsconcatrn 42555 naddgeoa 42608 mnuop3d 43493 fvelsetpreimafv 46514 opnneir 47701 |
Copyright terms: Public domain | W3C validator |