Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > r19.42v | GIF version |
Description: Restricted version of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 27-May-1998.) |
Ref | Expression |
---|---|
r19.42v | ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.41v 2587 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
2 | ancom 264 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
3 | 2 | rexbii 2442 | . 2 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ ∃𝑥 ∈ 𝐴 (𝜓 ∧ 𝜑)) |
4 | ancom 264 | . 2 ⊢ ((𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜓 ∧ 𝜑)) | |
5 | 1, 3, 4 | 3bitr4i 211 | 1 ⊢ (∃𝑥 ∈ 𝐴 (𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥 ∈ 𝐴 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∃wrex 2417 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-rex 2422 |
This theorem is referenced by: ceqsrexbv 2816 ceqsrex2v 2817 2reuswapdc 2888 iunrab 3860 iunin2 3876 iundif2ss 3878 iunopab 4203 elxp2 4557 cnvuni 4725 elunirn 5667 f1oiso 5727 oprabrexex2 6028 genpdflem 7315 1idprl 7398 1idpru 7399 ltexprlemm 7408 rexuz2 9376 4fvwrd4 9917 divalgb 11622 |
Copyright terms: Public domain | W3C validator |