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 2238 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 1955 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓)) | |
2 | 19.42v 1954 | . 2 ⊢ (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) | |
3 | 1, 2 | bitri 277 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∃wex 1780 |
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 1911 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 |
This theorem is referenced by: exdistr2 1959 19.42vvvOLD 1961 3exdistr 1962 ceqsex3v 3537 ceqsex4v 3538 ceqsex8v 3540 elvvv 5613 xpdifid 6011 dfoprab2 7198 resoprab 7256 elrnmpores 7274 ov3 7297 ov6g 7298 oprabex3 7664 xpassen 8597 axaddf 10553 axmulf 10554 qqhval2 31230 bnj996 32235 inxpxrn 35675 dvhopellsm 38285 |
Copyright terms: Public domain | W3C validator |