![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 19.42vv | Structured version Visualization version GIF version |
Description: Version of 19.42 2280 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 16-Mar-1995.) |
Ref | Expression |
---|---|
19.42vv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exdistr 2053 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
2 | 19.42v 2052 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) | |
3 | 1, 2 | bitri 267 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 386 ∃wex 1878 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 |
This theorem is referenced by: 19.42vvv 2057 exdistr2 2058 3exdistr 2059 ceqsex3v 3463 ceqsex4v 3464 ceqsex8v 3466 elvvv 5415 xpdifid 5807 dfoprab2 6966 resoprab 7021 elrnmpt2res 7039 ov3 7062 ov6g 7063 oprabex3 7422 xpassen 8329 axaddf 10289 axmulf 10290 qqhval2 30567 bnj996 31567 cnfinltrel 33781 inxpxrn 34696 dvhopellsm 37187 |
Copyright terms: Public domain | W3C validator |