| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 19.37v | Structured version Visualization version GIF version | ||
| Description: Version of 19.37 2232 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
| Ref | Expression |
|---|---|
| 19.37v | ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.35 1877 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) | |
| 2 | 19.3v 1981 | . . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑) | |
| 3 | 2 | imbi1i 349 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓)) |
| 4 | 1, 3 | bitri 275 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: spc3egv 3603 eqvincg 3648 rmoanim 3894 rmoanimALT 3895 axrep5 5287 fvn0ssdmfun 7094 kmlem14 10204 kmlem15 10205 bnj132 34740 bnj1098 34797 bnj150 34890 bnj865 34937 bnj996 34970 bnj1021 34980 bnj1090 34993 bnj1176 35019 sn-axrep5v 42255 cnvssco 43619 refimssco 43620 19.37vv 44404 pm11.61 44412 relopabVD 44921 |
| Copyright terms: Public domain | W3C validator |