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 1461 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | 1 | r19.41 2509 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∃wrex 2349 |
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 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-rex 2354 |
This theorem is referenced by: r19.42v 2511 3reeanv 2524 reuind 2795 iuncom4 3685 dfiun2g 3710 iunxiun 3757 inuni 3930 xpiundi 4416 xpiundir 4417 imaco 4846 coiun 4850 abrexco 5419 imaiun 5420 isoini 5477 rexrnmpt2 5636 genpassl 6714 genpassu 6715 4fvwrd4 9150 |
Copyright terms: Public domain | W3C validator |