![]() |
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 1462 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | rexbida 2369 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∈ wcel 1434 ∃wrex 2354 |
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 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-17 1460 ax-ial 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-rex 2359 |
This theorem is referenced by: 2rexbiia 2388 2rexbidva 2395 rexeqbidva 2570 dfimafn 5298 funimass4 5300 fconstfvm 5455 fliftel 5512 fliftf 5518 f1oiso 5544 releldm2 5890 frecabcl 6096 qsinxp 6298 qliftel 6302 supisolem 6610 genpassl 6986 genpassu 6987 addcomprg 7040 mulcomprg 7042 1idprl 7052 1idpru 7053 archrecnq 7125 archrecpr 7126 caucvgprprlemexbt 7168 caucvgprprlemexb 7169 archsr 7230 cnegexlem3 7562 cnegex2 7564 recexre 7955 rerecclap 8095 creur 8313 creui 8314 nndiv 8356 arch 8562 nnrecl 8563 expnlbnd 9913 clim2 10496 clim2c 10497 clim0c 10499 climabs0 10520 climrecvg1n 10559 sumeq2d 10570 sumeq2 10571 nndivides 10583 alzdvds 10635 oddm1even 10655 oddnn02np1 10660 oddge22np1 10661 evennn02n 10662 evennn2n 10663 divalgb 10705 modremain 10709 |
Copyright terms: Public domain | W3C validator |