![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rexbidva | GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 | ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ)) |
Ref | Expression |
---|---|
rexbidva | ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1418 | . 2 ⊢ Ⅎxφ | |
2 | ralbidva.1 | . 2 ⊢ ((φ ∧ x ∈ A) → (ψ ↔ χ)) | |
3 | 1, 2 | rexbida 2315 | 1 ⊢ (φ → (∃x ∈ A ψ ↔ ∃x ∈ A χ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∈ wcel 1390 ∃wrex 2301 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-rex 2306 |
This theorem is referenced by: 2rexbiia 2334 2rexbidva 2341 rexeqbidva 2514 dfimafn 5165 funimass4 5167 fconstfvm 5322 fliftel 5376 fliftf 5382 f1oiso 5408 releldm2 5753 qsinxp 6118 qliftel 6122 genpassl 6507 genpassu 6508 addcomprg 6554 mulcomprg 6556 1idprl 6566 1idpru 6567 archrecnq 6635 archsr 6708 cnegexlem3 6985 cnegex2 6987 recexre 7362 rerecclap 7488 creur 7692 creui 7693 nndiv 7735 arch 7954 nnrecl 7955 expnlbnd 9026 |
Copyright terms: Public domain | W3C validator |