Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cbvex | GIF version |
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
cbvex.1 | ⊢ Ⅎ𝑦𝜑 |
cbvex.2 | ⊢ Ⅎ𝑥𝜓 |
cbvex.3 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvex | ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvex.1 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
2 | 1 | nfri 1499 | . 2 ⊢ (𝜑 → ∀𝑦𝜑) |
3 | cbvex.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | nfri 1499 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
5 | cbvex.3 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 2, 4, 5 | cbvexh 1735 | 1 ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 Ⅎwnf 1440 ∃wex 1472 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 |
This theorem depends on definitions: df-bi 116 df-nf 1441 |
This theorem is referenced by: sb8e 1837 cbvex2 1902 cbvmo 2046 mo23 2047 clelab 2283 cbvrexf 2675 issetf 2719 eqvincf 2837 rexab2 2878 cbvrexcsf 3094 abn0m 3419 rabn0m 3421 euabsn 3629 eluniab 3784 cbvopab1 4037 cbvopab2 4038 cbvopab1s 4039 intexabim 4113 iinexgm 4115 opeliunxp 4641 dfdmf 4779 dfrnf 4827 elrnmpt1 4837 cbvoprab1 5893 cbvoprab2 5894 opabex3d 6069 opabex3 6070 seq3f1olemp 10401 fsum2dlemstep 11331 bdsepnfALT 13475 strcollnfALT 13572 |
Copyright terms: Public domain | W3C validator |