![]() |
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 1528 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | rexbida 2472 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∈ wcel 2148 ∃wrex 2456 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-rex 2461 |
This theorem is referenced by: 2rexbiia 2493 2rexbidva 2500 rexeqbidva 2687 dfimafn 5564 funimass4 5566 fconstfvm 5734 fliftel 5793 fliftf 5799 f1oiso 5826 releldm2 6185 frecabcl 6399 qsinxp 6610 qliftel 6614 supisolem 7006 enumctlemm 7112 ismkvnex 7152 genpassl 7522 genpassu 7523 addcomprg 7576 mulcomprg 7578 1idprl 7588 1idpru 7589 archrecnq 7661 archrecpr 7662 caucvgprprlemexbt 7704 caucvgprprlemexb 7705 archsr 7780 map2psrprg 7803 suplocsrlempr 7805 axsuploc 8028 cnegexlem3 8132 cnegex2 8134 recexre 8533 rerecclap 8685 creur 8914 creui 8915 nndiv 8958 arch 9171 nnrecl 9172 expnlbnd 10641 fimaxq 10802 clim2 11286 clim2c 11287 clim0c 11289 climabs0 11310 climrecvg1n 11351 sumeq2 11362 mertensabs 11540 prodeq2 11560 zproddc 11582 nndivides 11799 alzdvds 11854 oddm1even 11874 oddnn02np1 11879 oddge22np1 11880 evennn02n 11881 evennn2n 11882 divalgb 11924 modremain 11928 modprmn0modprm0 12250 pythagtriplem2 12260 pythagtrip 12277 pceu 12289 mndpfo 12833 mndpropd 12835 grppropd 12887 dvdsr02 13267 crngunit 13273 dvdsrpropdg 13309 iscnp3 13634 lmbrf 13646 cncnp 13661 lmss 13677 metrest 13937 metcnp 13943 metcnp2 13944 txmetcnp 13949 cdivcncfap 14018 ivthdec 14053 pw1nct 14672 |
Copyright terms: Public domain | W3C validator |