![]() |
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 2220 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 1872 | . 2 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → ∃𝑥𝜓)) | |
2 | 19.3v 1977 | . . 3 ⊢ (∀𝑥𝜑 ↔ 𝜑) | |
3 | 2 | imbi1i 348 | . 2 ⊢ ((∀𝑥𝜑 → ∃𝑥𝜓) ↔ (𝜑 → ∃𝑥𝜓)) |
4 | 1, 3 | bitri 274 | 1 ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 ∃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 ax-6 1963 |
This theorem depends on definitions: df-bi 206 df-ex 1774 |
This theorem is referenced by: spc3egv 3592 eqvincg 3636 rmoanim 3889 rmoanimALT 3890 axrep5 5295 fvn0ssdmfun 7089 kmlem14 10194 kmlem15 10195 bnj132 34390 bnj1098 34447 bnj150 34540 bnj865 34587 bnj996 34620 bnj1021 34630 bnj1090 34643 bnj1176 34669 sn-axrep5v 41735 cnvssco 43067 refimssco 43068 19.37vv 43853 pm11.61 43861 relopabVD 44371 |
Copyright terms: Public domain | W3C validator |