![]() |
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 2224 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 1950 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
2 | 19.42v 1949 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) | |
3 | 1, 2 | bitri 274 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∃wex 1773 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 |
This theorem is referenced by: exdistr2 1954 3exdistr 1956 cgsex4g 3509 ceqsex3v 3521 ceqsex4v 3522 ceqsex8v 3524 elvvv 5753 xpdifid 6174 dfoprab2 7478 resoprab 7538 elrnmpores 7559 ov3 7584 ov6g 7585 oprabex3 7982 xpassen 9094 entrfil 9216 domtrfil 9223 sbthfilem 9229 axaddf 11175 axmulf 11176 catcone0 17686 qqhval2 33734 bnj996 34738 fineqvac 34868 inxpxrn 38017 dvhopellsm 40740 |
Copyright terms: Public domain | W3C validator |