| 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 1550 | . 2 ⊢ Ⅎ𝑥𝜑 | |
| 2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
| 3 | 1, 2 | rexbida 2500 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒)) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 ∈ wcel 2175 ∃wrex 2484 |
| 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 1469 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-4 1532 ax-17 1548 ax-ial 1556 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 df-rex 2489 |
| This theorem is referenced by: 2rexbiia 2521 2rexbidva 2528 rexeqbidva 2720 dfimafn 5626 funimass4 5628 fconstfvm 5801 fliftel 5861 fliftf 5867 f1oiso 5894 releldm2 6270 frecabcl 6484 qsinxp 6697 qliftel 6701 supisolem 7109 enumctlemm 7215 ismkvnex 7256 genpassl 7636 genpassu 7637 addcomprg 7690 mulcomprg 7692 1idprl 7702 1idpru 7703 archrecnq 7775 archrecpr 7776 caucvgprprlemexbt 7818 caucvgprprlemexb 7819 archsr 7894 map2psrprg 7917 suplocsrlempr 7919 axsuploc 8144 cnegexlem3 8248 cnegex2 8250 recexre 8650 rerecclap 8802 creur 9031 creui 9032 nndiv 9076 arch 9291 nnrecl 9292 expnlbnd 10807 fimaxq 10970 wrdval 10995 clim2 11536 clim2c 11537 clim0c 11539 climabs0 11560 climrecvg1n 11601 sumeq2 11612 mertensabs 11790 prodeq2 11810 zproddc 11832 nndivides 12050 alzdvds 12107 oddm1even 12128 oddnn02np1 12133 oddge22np1 12134 evennn02n 12135 evennn2n 12136 divalgb 12178 modremain 12182 modprmn0modprm0 12521 pythagtriplem2 12531 pythagtrip 12548 pceu 12560 4sqlem12 12667 gsumpropd2 13167 mndpfo 13212 mndpropd 13214 grppropd 13291 conjnmzb 13558 dvdsr02 13809 crngunit 13815 dvdsrpropdg 13851 cnfldui 14293 znunit 14363 iscnp3 14617 lmbrf 14629 cncnp 14644 lmss 14660 metrest 14920 metcnp 14926 metcnp2 14927 txmetcnp 14932 cdivcncfap 15018 ivthdec 15058 lgsquadlem2 15497 2lgslem1a 15507 pw1nct 15873 |
| Copyright terms: Public domain | W3C validator |