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 form). (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1508 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | rexbida 2432 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∈ wcel 1480 ∃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-nf 1437 df-rex 2422 |
This theorem is referenced by: 2rexbiia 2451 2rexbidva 2458 rexeqbidva 2641 dfimafn 5470 funimass4 5472 fconstfvm 5638 fliftel 5694 fliftf 5700 f1oiso 5727 releldm2 6083 frecabcl 6296 qsinxp 6505 qliftel 6509 supisolem 6895 enumctlemm 6999 ismkvnex 7029 genpassl 7332 genpassu 7333 addcomprg 7386 mulcomprg 7388 1idprl 7398 1idpru 7399 archrecnq 7471 archrecpr 7472 caucvgprprlemexbt 7514 caucvgprprlemexb 7515 archsr 7590 map2psrprg 7613 suplocsrlempr 7615 axsuploc 7837 cnegexlem3 7939 cnegex2 7941 recexre 8340 rerecclap 8490 creur 8717 creui 8718 nndiv 8761 arch 8974 nnrecl 8975 expnlbnd 10416 fimaxq 10573 clim2 11052 clim2c 11053 clim0c 11055 climabs0 11076 climrecvg1n 11117 sumeq2 11128 mertensabs 11306 prodeq2 11326 nndivides 11500 alzdvds 11552 oddm1even 11572 oddnn02np1 11577 oddge22np1 11578 evennn02n 11579 evennn2n 11580 divalgb 11622 modremain 11626 iscnp3 12372 lmbrf 12384 cncnp 12399 lmss 12415 metrest 12675 metcnp 12681 metcnp2 12682 txmetcnp 12687 cdivcncfap 12756 ivthdec 12791 |
Copyright terms: Public domain | W3C validator |