![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > r19.41v | GIF version |
Description: Restricted quantifier version of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 17-Dec-2003.) |
Ref | Expression |
---|---|
r19.41v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1462 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | 1 | r19.41 2510 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∃wrex 2350 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-rex 2355 |
This theorem is referenced by: r19.42v 2512 3reeanv 2525 reuind 2796 iuncom4 3693 dfiun2g 3718 iunxiun 3765 inuni 3938 xpiundi 4424 xpiundir 4425 imaco 4856 coiun 4860 abrexco 5430 imaiun 5431 isoini 5488 rexrnmpt2 5647 genpassl 6776 genpassu 6777 4fvwrd4 9227 |
Copyright terms: Public domain | W3C validator |