|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > 19.41vv | Structured version Visualization version GIF version | ||
| Description: Version of 19.41 2234 with two quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Apr-1995.) | 
| Ref | Expression | 
|---|---|
| 19.41vv | ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | 19.41v 1948 | . . 3 ⊢ (∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑦𝜑 ∧ 𝜓)) | |
| 2 | 1 | exbii 1847 | . 2 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ ∃𝑥(∃𝑦𝜑 ∧ 𝜓)) | 
| 3 | 19.41v 1948 | . 2 ⊢ (∃𝑥(∃𝑦𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | |
| 4 | 2, 3 | bitri 275 | 1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∃wex 1778 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 | 
| This theorem is referenced by: 19.41vvv 1950 cgsex4g 3527 rabxp 5732 copsex2gb 5815 mpomptx 7547 xpassen 9107 dfac5lem1 10164 fusgr2wsp2nb 30354 bnj996 34971 dfdm5 35774 dfrn5 35775 elima4 35777 brtxp2 35883 brpprod3a 35888 brimg 35939 brsuccf 35943 brxrn2 38377 diblsmopel 41174 en2pr 43565 mpomptx2 48256 | 
| Copyright terms: Public domain | W3C validator |