![]() |
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 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1421 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | rexbida 2321 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 ∈ wcel 1393 ∃wrex 2307 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-rex 2312 |
This theorem is referenced by: 2rexbiia 2340 2rexbidva 2347 rexeqbidva 2520 dfimafn 5222 funimass4 5224 fconstfvm 5379 fliftel 5433 fliftf 5439 f1oiso 5465 releldm2 5811 qsinxp 6182 qliftel 6186 genpassl 6622 genpassu 6623 addcomprg 6676 mulcomprg 6678 1idprl 6688 1idpru 6689 archrecnq 6761 archrecpr 6762 caucvgprprlemexbt 6804 caucvgprprlemexb 6805 archsr 6866 cnegexlem3 7188 cnegex2 7190 recexre 7569 rerecclap 7706 creur 7911 creui 7912 nndiv 7954 arch 8178 nnrecl 8179 expnlbnd 9373 clim2 9804 clim2c 9805 clim0c 9807 climabs0 9828 climrecvg1n 9867 |
Copyright terms: Public domain | W3C validator |